proposition: Lemma improve_pivotP m n (M : 'M_(1 + m, 1 + n)) : M 0 0 != 0 -> improve_pivot_spec M (improve_pivot M).
proof: Proof. move=> ?; rewrite /improve_pivot. have := (@improve_pivot_recP _ _ 1%:M M 1%:M (sdvdr_wf _)). case; rewrite ?unitmx1 // !invr1 mul1mx mulmx1 => ? ? ? eqM ? ? ? ? ?. by constructor=> //; rewrite eqM !mulmxA mulmxV // mul1mx mulmxKV. Qed.
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