proposition: Lemma find2P m n (A : 'M[E]_(m.+1, n.+1)) v : pick_spec [pred ij | ~~(v %| A ij.1 (lift 0 ij.2))] (find2 A v).
proof: Proof. exact: pickP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image)