proposition: Lemma sum_n_m_const_zero (n m : nat) : sum_n_m (fun _ => zero) n m = zero.
proof: Proof. rewrite /sum_n_m /iter_nat. elim: (seq.iota n (S m - n)) => //= h t ->. by apply plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub