proposition: Theorem iso_nat_iso : isomorphism h12 h21.
proof: Proof. unfold isomorphism. split. { apply Hom12.hom_nat_iso. } split. { apply Hom21.hom_nat_iso. } split. { apply Inverse12.inverse_nat_iso. } apply Inverse21.inverse_nat_iso. Qed.
imports: NBase