proposition: Lemma cmp_lt_iff : forall x y:A, cmp x y = Lt <-> lt x y.
proof: Proof. destruct lt_strict as [Hirr Htrans]; intros x y; destruct (cmp_ok x y);split; auto; try discriminate. intro ; subst y; destruct (Hirr x);auto. intro; destruct (Hirr x); eapply Htrans; eauto. Qed.
imports: Arith RelationClasses