fact: Definition improve_pivot k m n (M : 'M[E]_(1 + m, 1 + n)) := improve_pivot_rec k 1 M 1.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg ssrint ssrnum fintype choice) mathcomp(matrix mxalgebra bigop zmodp perm) dvdring mxstructure stronglydiscrete coherent edr