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