proposition: Lemma sum_n_plus : forall (u v : nat -> G) (n : nat), sum_n (fun k => plus (u k) (v k)) n = plus (sum_n u n) (sum_n v n).
proof: Proof. intros u v n. apply sum_n_m_plus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub