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