proposition: Lemma rfix_mxP m (W : 'M_(m, n)) (H : {set gT}) : reflect (forall x, x \in H -> W *m rG x = W) (W <= rfix_mx H)%MS.
proof: Proof. rewrite /rfix_mx; set C := \matrix_i _. apply: (iffP row_subP) => [cHW x Hx | cHW j]. apply/row_matrixP=> j; apply/eqP; rewrite -subr_eq0 row_mul. move/sub_kermxP: {cHW}(cHW j); rewrite mul_rV_lin1 /=; move/(canRL mxvecK). move/row_matrixP/(_ (enum_rank_in Hx x)); rewrite row_mul rowK !linear0. by rewrite enum_rankK_in // mul_vec_lin_row mulmxBr mulmx1 => ->. apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK). apply/row_matrixP=> i; rewrite row_mul rowK mul_vec_lin_row -row_mul. by rewrite mulmxBr mulmx1 cHW ?enum_valP // subrr !linear0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)