proposition: Lemma itersucc_or_itersucc n m : exists k, n == (S^k) m \/ m == (S^k) n.
proof: Proof. revert n. apply central_induction with (z:=m). { intros x y eq_xy; apply ex_iff_morphism. intros n; apply or_iff_morphism. + split; intros; etransitivity; try eassumption; now symmetry. + split; intros; (etransitivity; [eassumption|]); [|symmetry]; (eapply nat_rect_wd; [eassumption|apply succ_wd]). } - exists 0%nat. now left. - intros n. split; intros [k [L|R]]. + exists (Datatypes.S k). left. now apply succ_wd. + destruct k as [|k]. * simpl in R. exists 1%nat. left. now apply succ_wd. * rewrite nat_rect_succ_r in R. exists k. now right. + destruct k as [|k]; simpl in L. * exists 1%nat. now right. * apply succ_inj in L. exists k. now left. + exists (Datatypes.S k). right. now rewrite nat_rect_succ_r. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat