proposition: Lemma Sum_minus_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 a b. astepl (Sum a b (fun i : nat => f i[+] [--] (g i))). cut (Sum a b (fun i : nat => f i[+] (fun j : nat => [--] (g j)) i) [=] Sum a b f[+]Sum a b (fun j : nat => [--] (g j))). intro H. astepl (Sum a b f[+]Sum a b (fun j : nat => [--] (g j))). Step_final (Sum a b f[+] [--] (Sum a b g)). change (Sum a b (fun i : nat => f i[+] (fun j : nat => [--] (g j)) i) [=] Sum a b f[+]Sum a b (fun j : nat => [--] (g j))) in |- *. apply Sum_plus_Sum. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)