proposition: Lemma eval_mxrank e r m n (A : 'M_(m, n)) : qf_eval e (mxrank_form r A) = (\rank (eval_mx e A) == r).
proof: Proof. elim: m r n A => [|m IHm] r [|n] A /=; try by case r; rewrite unlock. rewrite GRing.eval_Pick !unlock /=; set pf := fun _ => _. rewrite -(@eq_pick _ pf) => [|k]; rewrite {}/pf ?mxE // eq_sym. case: pick => [[i j]|] //=; set B := _ - _; have:= mxrankE B. case: (Gaussian_elimination_ B) r => [[_ _] _] [|r] //= <-; rewrite {}IHm eqSS. by congr (\rank _ == r); apply/matrixP=> k l; rewrite !(mxE, big_ord1) !tpermR. 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)