proposition: Lemma sum_plus n m u : sum (n + m) u = sum n u + sum m (shift n u).
proof: Proof. revert u; induction n; intros u; simpl. - ring_simplify. apply sum_ext; compute; auto. - rewrite IHn. ring_simplify. f_equal. apply sum_ext; intros; unfold shift. f_equal; auto with *. Qed.
imports: Lia Reals Psatz