fact: Hypothesis find_pivotP : forall m n (E : 'M[E]_(1 + m,1 + n)), pick_spec [pred ij | E ij.1 ij.2 != 0] (find_pivot E).
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