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