proposition: Lemma ismon_scrr : is_CMonoid subcrr (Build_subcsetoid_crr _ _ _ Punit).
proof: Proof. split; red in |- *. intro x. case x. intros scs_elem scs_prf. apply (cm_rht_unit_unfolded scs_elem). intro x. case x. intros scs_elem scs_prf. apply (cm_lft_unit_unfolded scs_elem). 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