proposition: Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n.
proof: Proof. intros z n H. destruct (lt_exists_pred _ _ H) as (n' & EQ & LE). rewrite EQ. now rewrite pred_succ. Qed.
imports: NZAxioms NZBase Decidable OrdersTac