proposition: Lemma cm_Sum_units (a: list M): (forall x, In x a -> x [=] [0]) -> cm_Sum a [=] [0].
proof: Proof. Proof with intuition. clear D. induction a. intuition. intros E. simpl. rewrite IHa... rewrite (E a)... apply cm_lft_unit_unfolded. 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