proposition: Lemma sum_ext_lt n u v : (forall i, lt i n -> u i = v i) -> sum n u = sum n v.
proof: Proof. revert u v; induction n. auto. intros u v E; simpl; rewrite E; auto with *. f_equal. apply IHn. intros i Hi. apply E. lia. Qed.
imports: Lia Reals Psatz