proposition: Lemma psi_ler l e : (((2 ^ l).-1 + \sum_(i <- e) 2 ^ (minn (troot i) l))%:R - (l * 2 ^ l)%:R <= ((psi e)%:R : int))%R.
proof: Proof. have [/psi_aux_psib/le_trans->//|lLp] := leqP (psi_auxb e) l. rewrite [X in (_ <= X%:R)%R](bigD1 (Ordinal lLp)) //=. apply: le_trans (ler_rnz _) _. rewrite -natz ler_nat. apply: leq_maxl. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)