proposition: Lemma Sum_plus_Sum : forall f g m n, Sum m n (fun i => f i[+]g i) [=] Sum m n f[+]Sum m n g.
proof: Proof. intros f g m n. unfold Sum in |- *. unfold Sum1 in |- *. astepl (Sum0 (S n) f[+]Sum0 (S n) g[-] (Sum0 m f[+]Sum0 m g)). astepl (Sum0 (S n) f[+]Sum0 (S n) g[-]Sum0 m f[-]Sum0 m g). unfold cg_minus in |- *. astepr (Sum0 (S n) f[+] [--] (Sum0 m f) [+]Sum0 (S n) g[+] [--] (Sum0 m g)). apply bin_op_wd_unfolded. astepl (Sum0 (S n) f[+] (Sum0 (S n) g[+] [--] (Sum0 m f))). astepl (Sum0 (S n) f[+] ([--] (Sum0 m f) [+]Sum0 (S n) g)). algebra. algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)