no goals
α : Type u
l₁ l₂ : List α
H : length l₁ ≤ length l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
classical
exact Decidable.List.Lex.ne_iff H
no goals
α : Type u
l₁ l₂ : List α
H : length l₁ ≤ length l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
exact Decidable.List.Lex.ne_iff H