proposition: Lemma sum_n_m_ext (a b : nat -> G) n m : (forall n, a n = b n) -> sum_n_m a n m = sum_n_m b n m.
proof: Proof. intros H. by apply sum_n_m_ext_loc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub