proposition: Lemma inv_Sum0 : forall f n, Sum0 n (fun i => [--] (f i)) [=] [--] (Sum0 n f).
proof: Proof. intros f n. induction n as [| n Hrecn]. simpl in |- *; algebra. simpl in |- *. Step_final ([--] (Sum0 n f) [+] [--] (f n)). Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)