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