proposition: Lemma opp_mult_r : forall x y : K, opp (mult x y) = mult x (opp y).
proof: Proof. intros x y. apply plus_reg_l with (mult x y). rewrite plus_opp_r -mult_distr_l. now rewrite plus_opp_r mult_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub