proposition: Lemma cormen_lup_perm n (A : 'M_n.+1) : is_perm_mx (cormen_lup A).1.1.
proof: Proof. elim: n => [|n IHn] /= in A *; first exact: is_perm_mx1. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P L U]] {A'}/=. rewrite (is_perm_mxMr _ (perm_mx_is_perm _ _)). by case/is_perm_mxP => s ->; apply: lift0_mx_is_perm. 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)