fact: Definition R_Ring_mixin := Ring.Mixin _ _ _ (fun x y z => sym_eq (Rmult_assoc x y z)) Rmult_1_r Rmult_1_l Rmult_plus_distr_r Rmult_plus_distr_l.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub