proposition: Lemma scal_minus_distr_l (x : K) (u v : V) : scal x (minus u v) = minus (scal x u) (scal x v).
proof: Proof. by rewrite /minus scal_distr_l scal_opp_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub