proposition: Lemma cormen_lup_detL n (A : 'M_n.+1) : \det (cormen_lup A).1.2 = 1.
proof: Proof. elim: n => [|n IHn] /= in A *; first by rewrite det1. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P L U]] {A'}/= detL. by rewrite (@det_lblock _ 1) det1 mul1r. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype) mathcomp(div finfun bigop prime binomial ssralg finset fingroup finalg) mathcomp(mxalgebra perm zmodp matrix ssrint)