proposition: Lemma cm_Sum_eq {A} (a: list A) (f g: A -> M): (forall x, f x [=] g x) -> cm_Sum (map f a) [=] cm_Sum (map g a).
proof: Proof. Proof with try reflexivity. intro E. induction a... simpl. rewrite E, IHa... 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