proposition: Lemma sum_n_ext_loc : forall (a b : nat -> G) N, (forall n, (n <= N)%nat -> a n = b n) -> sum_n a N = sum_n b N.
proof: Proof. intros a b N H. apply sum_n_m_ext_loc => k [ _ Hk]. by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub