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