proposition: Lemma cormen_lup_lower n (A : 'M_n.+1) (i j : 'I_n.+1) : i <= j -> (cormen_lup A).1.2 i j = (i == j)%:R.
proof: Proof. elim: n => [|n IHn] /= in A i j *; first by rewrite [i]ord1 [j]ord1 mxE. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P L U]] {A'}/= Ll. rewrite !mxE split1; case: unliftP => [i'|] -> /=; rewrite !mxE split1. by case: unliftP => [j'|] -> //; exact: Ll. by case: unliftP => [j'|] ->; rewrite /= mxE. 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)