proposition: Theorem lt_asymm : forall n m, n < m -> ~ m < n.
proof: Proof. intros n m; nzinduct n m. - intros H; false_hyp H lt_irrefl. - intro n; split; intros H H1 H2. + apply lt_succ_r in H2. le_elim H2. * apply H; auto. apply le_succ_l. now apply lt_le_incl. * rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l. + apply le_succ_l in H1. le_elim H1. * apply H; auto. rewrite lt_succ_r. now apply lt_le_incl. * rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l. Qed.
imports: NZAxioms NZBase Decidable OrdersTac