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