proposition: Lemma sum_n_m_Reals a n m : (n <= m)%nat -> sum_n_m a n m = sum_f n m a.
proof: Proof. induction m => //= Hnm. apply Nat.le_0_r in Hnm. by rewrite Hnm sum_n_n /=. case: (le_dec n m) => H. rewrite sum_n_Sm // IHm //. rewrite sum_f_n_Sm //. replace n with (S m). rewrite sum_n_n. by rewrite /sum_f Nat.sub_diag /=. apply Nat.le_antisymm => //. apply not_le in H. by apply Nat.le_succ_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub