proposition: Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
proof: Proof. intros n m p; nzinduct p m. - intros _ H; false_hyp H lt_irrefl. - intro p. rewrite 2 lt_succ_r. split; intros H H1 H2. + apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1]. + assert (n <= p) as H3 by (auto using lt_le_incl). le_elim H3. * assumption. * rewrite <- H3 in H2. elim (lt_asymm n m); auto. Qed.
imports: NZAxioms NZBase Decidable OrdersTac