proposition: Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
proof: Proof. unfold lt; intros; apply Nat.lt_trans with y; auto. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec