proposition: Lemma succ_pred_approx : forall n, ~initial n -> S (P n) == n.
proof: Proof. intros n NB. rewrite initial_alt in NB. destruct (eq_decidable (S (P n)) n); auto. elim NB; auto. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat