proposition: Lemma initial_unique : forall m, initial m -> m == init.
proof: Proof. intros m Im. destruct (itersucc_or_itersucc init m) as (p,[H|H]). - destruct p. + now simpl in *. + destruct (Initial _ H). - destruct p. + now simpl in *. + destruct (Im _ H). Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat