proposition: Lemma e1e2_is_lft_unit: (is_lft_unit (dprod_as_csb_fun M1 M2)(pairT (@cm_unit M1)(@cm_unit M2))).
proof: Proof. intro x. case x. intros x1 x2. simpl. split. apply cm_lft_unit_unfolded. apply cm_lft_unit_unfolded. 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