proposition: Lemma cm_rht_unit_unfolded : forall x : M, x[+][0] [=] x.
proof: Proof. Proof cm_rht_unit M. Lemma cm_lft_unit_unfolded : forall x : M, [0][+]x [=] x. Proof cm_lft_unit M. Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra. Lemma cm_unit_unique_lft : forall x : M, is_lft_unit csg_op x -> x [=] [0]. Proof. intros x h. red in h. Step_final (x[+][0]). 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