proposition: Lemma cm_Sum_app: forall (k l : (list M)), (cm_Sum (app k l))[=] (cm_Sum k)[+](cm_Sum l).
proof: Proof. intros k l. induction k. simpl. apply eq_symmetric. apply cm_lft_unit_unfolded. simpl. astepr (a [+] ( (cm_Sum k)[+](cm_Sum l))). apply csbf_wd_unfolded. intuition. exact IHk. 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