proposition: Lemma power_plus:forall (M:CMonoid)(a:M)(m n:nat), (power_CMonoid a (m+n))[=] (power_CMonoid a m)[+](power_CMonoid a n).
proof: Proof. intros M a m n. induction m. simpl. apply eq_symmetric. apply cm_lft_unit. simpl. astepl (csbf_fun M M M (csg_op (c:=M)) a ((csbf_fun M M M (csg_op (c:=M)) (power_CMonoid a m) (power_CMonoid a n)))). algebra. 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