fact: Fixpoint improve_pivot_rec {m n} (P : 'M[R]_(1 + m)) (M : 'M[R]_(1 + m, 1 + n)) (Q : 'M[R]_(1 + n)) (k : Acc (@sdvdr [the dvdRingType of R]) (M 0 0)) : 'M[R]_(1 + m) * 'M[R]_(1 + m, 1 + n) * 'M[R]_(1 + n) := match k with Acc_intro IHa => if find1P M (M 0 0) is Pick i Hi then let Ai0 := M (lift 0 i) 0 in let P := Bezout_step (M 0 0) Ai0 P i in improve_pivot_rec P Q (IHa _ (sdvd_Bezout_step Hi)) else let u := dlsubmx M in let vM := ursubmx M in let vP := usubmx P in let u' := map_mx (fun x => 1 - odflt 0 (x %/? M 0 0)) u in let P := col_mx (usubmx P) (u' *m vP + dsubmx P) in let A := block_mx (M 0 0)%:M vM (const_mx (M 0 0)) (u' *m vM + drsubmx M) in if find2P A (M 0 0) is Pick (i,j) Hij then let A := xrow 0 i A in let P := xrow 0 i P in let a := A 0 0 in let A0j := A 0 (lift 0 j) in let Q := (Bezout_step a A0j Q^T j)^T in improve_pivot_rec P Q (IHa _ (sdvd_Bezout_step2 Hij)) else (P, A, Q) end.
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