proposition: Lemma cmp_eq_iff : forall x y:A, cmp x y = Eq <-> x = y.
proof: Proof. split. destruct lt_strict as [Hirr _]. destruct (cmp_ok x y); auto. - discriminate. - discriminate. - intro; subst y; now rewrite cmp_eq. Qed.
imports: Arith RelationClasses