proposition: Theorem le_succ_l : forall n m, S n <= m <-> n < m.
proof: Proof. intros n m; nzinduct m n. - split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl. - intro m. rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. rewrite or_cancel_r. + reflexivity. + intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l. + intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl. Qed.
imports: NZAxioms NZBase Decidable OrdersTac