fact: Definition prod_AbelianMonoid_mixin (U V : AbelianMonoid) := AbelianMonoid.Mixin (U * V) _ _ prod_plus_comm prod_plus_assoc prod_plus_zero_r.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub