proposition: Lemma initial_ancestor : forall m, exists p, m == (S^p) init.
proof: Proof. intros m. destruct (itersucc_or_itersucc init m) as (p,[H|H]). - destruct p; simpl in *; auto. + exists O; auto with *. + destruct (Initial _ H). - exists p; auto. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat