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