proposition: Theorem natural_isomorphism_succ : forall n : N1.t, natural_isomorphism (N1.succ n) == N2.succ (natural_isomorphism n).
proof: Proof. unfold natural_isomorphism. intro n. rewrite N1.recursion_succ; auto with *. repeat red; intros. now f_equiv. Qed.
imports: NBase