fact: Fixpoint Gaussian_elimination_ {F : fieldType} {m n} : 'M[F]_(m, n) -> 'M_m * 'M_n * nat := match m, n with | _.+1, _.+1 => fun A : 'M_(1 + _, 1 + _) => if [pick ij | A ij.1 ij.2 != 0] is Some (i, j) then let a := A i j in let A1 := xrow i 0 (xcol j 0 A) in let u := ursubmx A1 in let v := a^-1 *: dlsubmx A1 in let: (L, U, r) := Gaussian_elimination_ (drsubmx A1 - v *m u) in (xrow i 0 (block_mx 1 0 v L), xcol j 0 (block_mx a%:M u 0 U), r.+1) else (1%:M, 1%:M, 0) | _, _ => fun _ => (1%:M, 1%:M, 0) end.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)