proposition: Lemma cormen_lup_upper n A (i j : 'I_n.+1) : j < i -> (cormen_lup A).2 i j = 0 :> F.
proof: Proof. elim: n => [|n IHn] /= in A i j *; first by rewrite [i]ord1. set A' := _ - _; move/(_ A'): IHn; case: cormen_lup => [[P L U]] {A'}/= Uu. rewrite !mxE split1; case: unliftP => [i'|] -> //=; rewrite !mxE split1. by case: unliftP => [j'|] ->; [apply: Uu | rewrite /= mxE]. 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)