proposition: Lemma cmp_sym : forall x y , cmp x y = Gt <-> cmp y x = Lt.
proof: Proof. destruct lt_strict as [Hirr Htrans]. intros x y;destruct (cmp_ok x y);destruct (cmp_ok y x); split;try discriminate;auto;intros. - subst y; now destruct (Hirr x). - destruct (Hirr x); transitivity y;auto. - subst y; now destruct (Hirr x). - destruct (Hirr x); transitivity y;auto. Qed.
imports: Arith RelationClasses