proposition: Lemma sum_n_m_sum_n (a:nat -> G) (n m : nat) : (n <= m)%nat -> sum_n_m a (S n) m = minus (sum_n a m) (sum_n a n).
proof: Proof. intros Hnm. apply plus_reg_l with (sum_n a n). rewrite (plus_comm _ (minus _ _)) /minus -plus_assoc plus_opp_l plus_zero_r. rewrite /sum_n /sum_n_m. apply sym_eq, sum_n_m_Chasles. by apply Nat.le_0_l. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub