proposition: Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
proof: Proof. intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. - left; eauto with ordered_type. - left; eapply MO1.lt_eq; eauto. - left; eapply MO1.eq_lt; eauto. - right; split; eauto with ordered_type. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec