proposition: Lemma psi_exp e : psi e <= (2 ^ #|`e|).-1.
proof: Proof. rewrite -(ler_nat (Num.NumDomain.clone _ int)). have [l ->] := psiE e. apply: le_trans (_ : ((2 ^ l).-1 + \sum_(i <- e) 2 ^ l)%:R - (l * 2 ^ l)%:R <= _)%R. apply: lerB => //. rewrite ler_nat leq_add2l. apply: leq_sum => i Hi. by rewrite leq_exp2l // geq_minr. rewrite fsum_nat_const lerBlDr -natrD ler_nat [X in _ <= X]addnC. rewrite -prednDl ?expn_gt0 // -prednDr ?expn_gt0 //. rewrite -!subn1 leq_sub2r //. have [E|E] := leqP #|`e| l. rewrite -(subnK E). set u := _ - _. rewrite expnD !mulnDl addnAC leq_add2r. case: u => [|u]; first by rewrite mul1n. by rewrite mulSn -addnA leq_addr. rewrite -(subnK (ltnW E)). set u := _ - _. rewrite expnD !mulnDl addnA addnC leq_add2l. by rewrite -mulSn leq_mul2r ltn_expl // orbT. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)