proposition: Lemma Sum0_shift : forall f g n, (forall i, f i [=] g (S i)) -> g 0[+]Sum0 n f [=] Sum0 (S n) g.
proof: Proof. intros a b l H. induction l as [| l Hrecl]. simpl in |- *; algebra. simpl in |- *. astepl (b 0[+]Sum0 l a[+]a l). Step_final (Sum0 (S l) b[+]a l). Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)