proposition: Lemma restrictM : {in [pred f | (V *m f <= V)%MS] &, {morph restrict : f g / f *m g}}.
proof: Proof. move=> f g; rewrite !inE => Vf Vg /=. by rewrite /restrict 2!mulmxA mulmxA mulmxKpV ?stable_row_base. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)