proposition: Lemma succ_onto_gives_succ_pred : forall n, S (P n) == n.
proof: Proof. intros n. destruct (succ_onto n) as (m,H). rewrite H, pred_succ; auto with *. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat