proposition: Lemma sum_f_rw_0 (u : nat -> R) (n : nat) : sum_f O n u = sum_f_R0 u n.
proof: Proof. rewrite /sum_f Nat.sub_0_r. elim: n => [ | n IH] //. rewrite /sum_f_R0 -/sum_f_R0 //. by rewrite Nat.add_0_r IH. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)