proposition: Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
proof: Proof. induction x; intros y z H1 H2. - destruct y as [| b y']; inversion H1. destruct z as [| c z']; inversion H2; constructor. - destruct y as [| b y']; inversion H1; subst; destruct z as [| c z']; inversion H2; subst. + constructor. eapply IHx; eauto. + constructor; assumption. + constructor; assumption. + constructor. eapply Nat.lt_trans; eassumption. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec