proposition: Lemma scal_minus_distr_r (x y : K) (u : V) : scal (minus x y) u = minus (scal x u) (scal y u).
proof: Proof. by rewrite /minus scal_distr_r scal_opp_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub