proposition: Lemma inverse_nat_iso : forall n : N1.t, h21 (h12 n) == n.
proof: Proof. induct n. - now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0. - intros n IH. now rewrite Hom12.natural_isomorphism_succ, Hom21.natural_isomorphism_succ, IH. Qed.
imports: NBase