proposition: Lemma ofnat_pred : forall n, n<>O -> [Peano.pred n] == P [n].
proof: Proof. unfold ofnat. destruct n. - destruct 1; auto. - intros _. simpl. symmetry. apply pred_succ. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat