English
Under a DecidableEq assumption, for all lists l1,l2 with length constraint, Lex (≠) l1 l2 iff l1 ≠ l2.
Русский
При предположении DecidableEq, для любых списков l1,l2 и ограничении по длине выполняется Lex (≠) l1 l2 ↔ l1 ≠ l2.
LaTeX
$$$\\forall l_1\\ l_2,\\ (\\text{IsDecidableEq }\\alpha)\\Rightarrow\\ \\mathrm{Lex}(\\neq)\\ l_1\\ l_2\\ \\iff\\ l_1 \\neq l_2.$$$
Lean4
theorem _root_.Decidable.List.Lex.ne_iff [DecidableEq α] {l₁ l₂ : List α} (H : length l₁ ≤ length l₂) :
Lex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂ :=
⟨to_ne, fun h => by
induction l₁ generalizing l₂ <;> rcases l₂ with - | ⟨b, l₂⟩
· contradiction
· apply nil
· exact (not_lt_of_ge H).elim (succ_pos _)
case cons.cons a l₁ IH =>
by_cases ab : a = b
· subst b
exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
· exact .rel ab⟩
