proposition: Lemma psi_max e l : (psi_aux l e <= (psi e)%:R)%R.
proof: Proof. pose n := maxn (psi_auxb e) l.+1. have /psiE_leq-> : psi_auxb e <= n by apply: leq_maxl. have O : l < n by apply: leq_maxr. have [/le_trans->//|/ltW/rnz_ger0->] := lerP (psi_aux l e) 0. rewrite ler_nat. by rewrite (bigD1 (Ordinal O)) //= leq_maxl. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)