proposition: Lemma sum_n_m_const (n m : nat) (a : R) : sum_n_m (fun _ => a) n m = INR (S m - n) * a.
proof: Proof. rewrite /sum_n_m /iter_nat (iter_const _ a). by rewrite -{2}(seq.size_iota n (S m - n)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub