Theorem: algebra.Order.lex_true_of_ble_lex_true
Proof state before:
case h_2.inl.inl
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : x = y
h :
  algebra.Order.ble_lex_impl (tail { val := x :: xs, property := property✝³ })
      (tail { val := y :: ys, property := property✝² }) =
    true
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝
Tactic:
exact aux (m-1) (tail ⟨x::xs, _⟩) (tail ⟨y::ys, _⟩) h
Proof state after:
case h_2.inl.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝² : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝¹ : x✝ = y✝
h✝ : ¬x = y
h : x ≤ y
⊢ lex_impl (tail { val := x :: xs, property := property✝³ }) (tail { val := y :: ys, property := property✝² })

case h_2.inr
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝¹ : algebra.Order.ble_lex_impl v₁ v₂ = true
m : ℕ
a b : Vector ℕ m
x : ℕ
xs : List ℕ
property✝³ : List.length (x :: xs) = m
y : ℕ
ys : List ℕ
property✝² : List.length (y :: ys) = m
h :
  algebra.Order.ble_lex_impl { val := x :: xs, property := property✝³ } { val := y :: ys, property := property✝² } =
    true
v₁✝ v₂✝ : Vector ℕ m
x✝ : ℕ
tail✝¹ : List ℕ
property✝¹ : List.length (x✝ :: tail✝¹) = m
y✝ : ℕ
tail✝ : List ℕ
property✝ : List.length (y✝ :: tail✝) = m
heq✝¹ : { val := x :: xs, property := property✝³ } = { val := x✝ :: tail✝¹, property := property✝¹ }
heq✝ : { val := y :: ys, property := property✝² } = { val := y✝ :: tail✝, property := property✝ }
h✝ : ¬x✝ = y✝
⊢ x✝ ≤ y✝