proposition: Lemma ofnat_injective : forall n m, [n]==[m] -> n = m.
proof: Proof. induction n as [|n IH]; destruct m; auto. - intros H; elim (ofnat_S_neq_0 _ H). - intros H; symmetry in H; elim (ofnat_S_neq_0 _ H). - intros. f_equal. apply IH. now rewrite <- succ_inj_wd. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat