proposition: Lemma initial_alt : forall n, initial n <-> S (P n) ~= n.
proof: Proof. split. - intros Bn EQ. symmetry in EQ. destruct (Bn _ EQ). - intros NEQ m EQ. apply NEQ. rewrite EQ, pred_succ; auto with *. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat