proposition: Lemma succ_swap_pred : forall k n m, n == (S^k) m -> m == (P^k) n.
proof: Proof. induction k. - simpl; auto with *. - simpl; intros. apply pred_wd in H. rewrite pred_succ in H. apply IHk in H; auto. rewrite <- nat_rect_succ_r in H; auto. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat