fact: Definition direct_product_is_CMonoid:= (Build_is_CMonoid (direct_product_as_CSemiGroup M1 M2) (pairT (@cm_unit M1)(@cm_unit M2)) e1e2_is_rht_unit e1e2_is_lft_unit).
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