fact: Definition prod_ModuleSpace_mixin (K : Ring) (U V : ModuleSpace K) := ModuleSpace.Mixin K _ _ (@prod_scal_assoc K U V) prod_scal_one prod_scal_distr_l prod_scal_distr_r.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub