proposition: Lemma scal_zero_l : forall u : V, scal zero u = zero.
proof: Proof. intros u. apply plus_reg_r with (r := scal zero u). rewrite plus_zero_l. rewrite <- scal_distr_r. now rewrite plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub