proposition: Lemma list_nat_eq_correct l1 l2 : if list_nat_eq l1 l2 then l1 = l2 else l1 <> l2.
proof: Proof. revert l2. induction l1 as [| n1 l1 Hrec]; destruct l2 as [| n2 l2]; simpl; try (intros; discriminate); auto. destruct (Nat.eqb_spec n1 n2) as [n1En2|H1]. generalize (Hrec l2); case list_nat_eq; intros H2. apply f_equal2 with (f := @cons _); auto. intros HH; case H2; injection HH; auto. intros HH; case H1; injection HH; auto. Qed.
imports: List ListAux UList OrderedList