proposition: Lemma isabgrp_scrr : is_CAbMonoid subcrr.
proof: Proof. red in |- *. intros x y. case x. case y. intros. simpl in |- *. apply cam_commutes_unfolded. Qed.
imports: CoRN.algebra.CMonoids CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms