proposition: Lemma cmp_eq : forall x:A, cmp x x = Eq.
proof: Proof. destruct lt_strict as [Hirr _]. intro x; destruct (cmp_ok x x). - reflexivity. - now destruct (Hirr x). - now destruct (Hirr x). Qed.
imports: Arith RelationClasses