proposition: Lemma isomorphic_PM1M2_PM2M1: (isomorphic (direct_product_as_CMonoid M1 M2) (direct_product_as_CMonoid M2 M1)):CProp.
proof: Proof. unfold isomorphic. simpl. exists f_as_CSetoid_fun_. unfold isomorphism. unfold morphism. simpl. split. split. intuition. intros a b. case a. intros a0 a1. case b. intros b0 b1. simpl. intuition. unfold bijective. split. unfold injective. simpl. intros a0 a1. elim a0. intros b0 b1. elim a1. intros c0 c1. simpl. intuition. unfold surjective. intro b. elim b. intros a0 a1. exists (pairT a1 a0). simpl. intuition. Qed.
imports: Coq.Arith.Euclid CoRN.model.Zmod.Cmod CoRN.algebra.CSemiGroups CoRN.tactics.csetoid_rewrite CoRN.model.structures.Nsec CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms