proposition: Lemma not_neq_eq : forall x y, ~~x==y -> x==y.
proof: Proof. intros x y H. destruct (P.lt_total x y) as [H'|[H'|H']]; auto; destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto. Qed.
imports: Setoid Morphisms Basics Equalities Orders