fact: Record mixin_of (K : Ring) (V : AbelianGroup) := Mixin { scal : K -> V -> V ; ax1 : forall x y u, scal x (scal y u) = scal (mult x y) u ; ax2 : forall u, scal one u = u ; ax3 : forall x u v, scal x (plus u v) = plus (scal x u) (scal x v) ; ax4 : forall x y u, scal (plus x y) u = plus (scal x u) (scal y u) }.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub