proposition: Lemma eval_submx e : qf_eval e submx_form = (eval_mx e A <= eval_mx e B)%MS.
proof: Proof. rewrite (morphAnd (qf_eval e)) //= big_andE /=. apply/forallP/idP=> /= [|sAB d]; last first. rewrite !eval_mxrank eval_col_mx -addsmxE; apply/implyP=> /eqP <-. by rewrite mxrank_leqif_sup ?addsmxSr // addsmx_sub sAB /=. move/(_ (inord (\rank (eval_mx e (col_mx A B))))). rewrite inordK ?ltnS ?rank_leq_col // !eval_mxrank eqxx /= eval_col_mx. by rewrite -addsmxE mxrank_leqif_sup ?addsmxSr // addsmx_sub; case/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)