proposition: Lemma psi_delta e s a : #|` e `\` `[delta s]| <= s -> a \in e -> psi e - psi (e `\ a) <= 2 ^ s.-1.
proof: Proof. move=> CLs aIe. rewrite leq_subLR -(ler_nat (Num.NumDomain.clone _ int)) natrD addrC -lerBlDr. have [l Hl] := psiE e. have F l1 : s <= l1.+1 -> (psi_aux l1.+1 e <= psi_aux l1 e)%R. move=> sLl1. rewrite psi_auxE_le. rewrite psi_auxE_lt. set s1 := \sum_(_ <- _ | _) _. have -> : [fset i in e | l1 < troot i] = [fset i in e | delta l1.+1 <= i]. by apply/fsetP => i; rewrite !inE root_delta_le. set c := #|`_|. have Hc : c <= s. apply: leq_trans CLs. apply: fsubset_leq_card. apply/fsubsetP=> i. rewrite !inE => /andP[-> H]. rewrite andbT mem_sint -leqNgt (leq_trans _ H) //. by apply: delta_le. rewrite expnS mulnAC [2 * _ * _]mulnC. rewrite mul2n mulnA muln2 -!addnn -[(_ + l1.+1)%N]addSnnS. rewrite mulnDl mulnDr prednDr ?(muln_gt0, expn_gt0) //. set x := 2 ^ _ * _. rewrite -[(_ + s1)%N]addnA [(x + _)%N]addnC. rewrite [X in (_ - X <= _)%R]natrD opprD addrA lerD //. rewrite lerBlDr natrD lerD // ler_nat. by rewrite mulnC leq_mul2l ltnS (leq_trans _ sLl1) ?orbT. pose l1 := minn l s.-1. have -> : ((psi e)%:R = psi_aux l1 e)%R. have [/minn_idPl U|E] := leqP l s.-1; first by rewrite [l1]U. have /ltnW/minn_idPr U := E. rewrite [l1]U. apply/eqP; rewrite eq_le psi_max andbT Hl. rewrite -(subnK (ltnW E)). elim: (_ - _) => [|k IH] //. apply: le_trans IH. rewrite addSn. apply: F => //. case: (s) => // s1. by rewrite ltnS /= leq_addl. apply: le_trans (lerB (lexx _) (psi_max _ l1)) _. rewrite /psi_aux opprB addrA subrK addnC !natrD opprD addrA addrK. rewrite lerBlDr -natrD ler_nat addnC -leq_subLR. rewrite (big_fsetD1 a) //= addnK leq_exp2l //. by apply: leq_trans (geq_minr _ _) (geq_minr _ _). Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)