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