proposition: Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
proof: Proof. intros (x1,x2) (y1,y2); unfold eq, lt; simpl; intuition. - apply (O1.lt_not_eq H0 H1). - apply (O2.lt_not_eq H3 H2). Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec