proposition: Lemma succ_onto_pred_injective : forall n m, P n == P m -> n == m.
proof: Proof. intros n m. intros H; apply succ_wd in H. rewrite !succ_onto_gives_succ_pred in H; auto. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat