fact: Variable find1 : forall m n, 'M[E]_(m.+1,n.+1) -> E -> option 'I_m.
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