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