proposition: Lemma cormen_lup_correct n (A : 'M_n.+1) : let: (P, L, U) := cormen_lup A in P * A = L * U.
proof: Proof. elim: n => [|n IHn] /= in A *; first by rewrite !mul1r. set k := odflt _ _; set A1 : 'M_(1 + _) := xrow _ _ _. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P' L' U']] /= IHn. rewrite -mulrA -!mulmxE -xrowE -/A1 /= -[n.+2]/(1 + n.+1)%N -{1}(submxK A1). rewrite !mulmx_block !mul0mx !mulmx0 !add0r !addr0 !mul1mx -{L' U'}[L' *m _]IHn. rewrite -scalemxAl !scalemxAr -!mulmxA addrC -mulrDr {A'}subrK. congr (block_mx _ _ (_ *m _) _). rewrite [_ *: _]mx11_scalar !mxE lshift0 tpermL {}/A1 {}/k. case: pickP => /= [k nzAk0 | no_k]; first by rewrite mulVf ?mulmx1. rewrite (_ : dlsubmx _ = 0) ?mul0mx //; apply/colP=> i. by rewrite !mxE lshift0 (elimNf eqP (no_k _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)