proposition: Lemma sum_n_m_Chasles (a : nat -> G) (n m k : nat) : (n <= S m)%nat -> (m <= k)%nat -> sum_n_m a n k = plus (sum_n_m a n m) (sum_n_m a (S m) k).
proof: Proof. intros Hnm Hmk. apply iter_nat_Chasles. by apply plus_zero_l. by apply plus_assoc. by []. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub