proposition: Theorem lt_exists_pred : forall z n, z < n -> exists k, n == S k /\ z <= k.
proof: Proof. intros z n Hzn. assert (exists m, n <= m) as [m Hnm] by now exists n. revert n Hzn Hnm. nzinduct m z. - order. - intro m; split; intros IH n H1 H2. + apply le_succ_r in H2. destruct H2 as [H2 | H2]. * now apply IH. * exists m. now split; [| rewrite <- lt_succ_r; rewrite <- H2]. + apply IH. * assumption. * now apply le_le_succ_r. Qed.
imports: NZAxioms NZBase Decidable OrdersTac