proposition: Lemma prod_scal_distr_r : forall (x y : K) (u : U * V), prod_scal (plus x y) u = prod_plus (prod_scal x u) (prod_scal y u).
proof: Proof. intros x y u. apply (f_equal2 pair) ; apply scal_distr_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub