fact: Fixpoint improve_pivot_rec k {m n} : 'M[E]_(1 + m) -> 'M[E]_(1 + m, 1 + n) -> 'M[E]_(1 + n) -> 'M[E]_(1 + m) * 'M[E]_(1 + m, 1 + n) * 'M[E]_(1 + n) := if k is p.+1 then fun P M Q => let a := M 0 0 in if find1 M a is Some i then let Mi0 := M (lift 0 i) 0 in let P := Bezout_step a Mi0 P i in let M := Bezout_step a Mi0 M i in improve_pivot_rec p P M Q 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 %/? a)) u in let P := col_mx (usubmx P) (u' *m vP + dsubmx P) in let M := block_mx (a%:M) vM (const_mx a) (u' *m vM + drsubmx M) in if find2 M a is Some (i,j) then let M := xrow 0 i M in let P := xrow 0 i P in let a := fun_of_matrix M 0 0 in let M0ij := fun_of_matrix M 0 (lift 0 j) in let Q := (Bezout_step a M0ij Q^T j)^T in let M := (Bezout_step a M0ij M^T j)^T in improve_pivot_rec p P M Q else (P, M, Q) else fun P M Q => (P,M,Q).
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