fact: Definition AbsRing_NormedModule_mixin := NormedModule.Mixin K _ abs 1 abs_triangle abs_mult (fun x y e H => H) AbsRing_norm_compat2 abs_eq_zero.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub