proposition: Lemma mult_zero_r : forall x : K, mult x zero = zero.
proof: Proof. intros x. apply plus_reg_r with (mult x zero). rewrite <- mult_distr_l. rewrite plus_zero_r. now rewrite plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub