fact: Definition PS_as_CMonoid (A : CSetoid) := Build_SubCMonoid (FS_as_CMonoid A) (bijective (A:=A) (B:=A)) ( id_is_bij A) (comp_resp_bij A A A).
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