proposition: Lemma list_compare_eq l l' : list_compare l l' = Eq <-> Forall2 (fun a a' => cmp a a' = Eq) l l'.
proof: Proof. split. - revert l'. induction l as [|a l IH]; destruct l' as [|b l']; simpl; try easy. rewrite lex_Eq; intuition. - induction 1; simpl; now rewrite ?lex_Eq. Qed.
imports: Coq(List)