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