proposition: Lemma scal_opp_r : forall (x : K) (u : V), scal x (opp u) = opp (scal x u).
proof: Proof. intros x u. apply plus_reg_r with (r := (scal x u)). rewrite plus_opp_l. rewrite <- scal_distr_l. rewrite plus_opp_l. apply scal_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub