proposition: Lemma prod_plus_assoc : forall x y z : U * V, prod_plus x (prod_plus y z) = prod_plus (prod_plus x y) z.
proof: Proof. intros x y z. apply (f_equal2 pair) ; apply plus_assoc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub