proposition: Lemma sum_Sn_m (a : nat -> G) (n m : nat) : (n <= m)%nat -> sum_n_m a n m = plus (a n) (sum_n_m a (S n) m).
proof: Proof. intros Hnmk. rewrite (sum_n_m_Chasles _ _ n). by rewrite sum_n_n. by apply Nat.le_succ_diag_r. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub