proposition: Lemma Sum0_plus_Sum0 : forall f g m, Sum0 m (fun i => f i[+]g i) [=] Sum0 m f[+]Sum0 m g.
proof: Proof. intros f g m. elim m. simpl in |- *; algebra. intros n H. simpl in |- *. astepl (Sum0 n f[+]Sum0 n g[+] (f n[+]g n)). astepl (Sum0 n f[+] (Sum0 n g[+] (f n[+]g n))). astepl (Sum0 n f[+] (Sum0 n g[+]f n[+]g n)). astepl (Sum0 n f[+] (f n[+]Sum0 n g[+]g n)). astepl (Sum0 n f[+] (f n[+]Sum0 n g) [+]g n). Step_final (Sum0 n f[+]f n[+]Sum0 n g[+]g n). Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)