proposition: Lemma Sum_big_shift : forall f g k m n, (forall j, m <= j -> f j [=] g (j + k)) -> m <= S n -> Sum m n f [=] Sum (m + k) (n + k) g.
proof: Proof. do 3 intro; generalize f g; clear f g. induction k as [| k Hreck]. intros f g n m. repeat rewrite <- plus_n_O. intros H H0. apply: Sum_wd'. auto. intros. set (Hi:= H i). rewrite <- (plus_n_O i) in Hi. apply: Hi. auto. intros; repeat rewrite <- plus_n_Sm. apply eq_transitive_unfolded with (Sum (m + k) (n + k) (fun n : nat => g (S n))). 2: apply Sum_shift; algebra. apply Hreck. intros; rewrite plus_n_Sm; apply H; auto with arith. auto. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)