fact: Fixpoint mxrank_form (r m n : nat) : 'M_(m, n) -> form := match m, n return 'M_(m, n) -> form with | m'.+1, n'.+1 => fun A : 'M_(1 + m', 1 + n') => let nzA k := A k.1 k.2 != 0 in let xSchur k := Schur (xrow k.1 0%R (xcol k.2 0%R A)) in let recf k := Bool (r > 0) /\ mxrank_form r.-1 (xSchur k) in GRing.Pick nzA recf (Bool (r == 0%N)) | _, _ => fun _ => Bool (r == 0%N) end%T.
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)