proposition: Lemma psi_aux_card_le l e : (psi_aux l `[#|`e|] <= psi_aux l e)%R.
proof: Proof. rewrite lerB // ler_nat leq_add2l. rewrite (sum_sint (fun i => 2 ^ minn (∇i) l)) //. have [n cI] := ubnP #|`e|; elim: n => // [] [|n] IH e cI in e cI *. by move: cI; rewrite ltnS leqn0 => /eqP-> ; rewrite big_ord0. move: cI; rewrite leq_eqVlt => /orP[/eqP [] eC|]; last first. by apply: IH. have /(eq_fbigmax id)[/= i [iIe iM]] : 0 < #|`e| by rewrite -ltnS eC. have eE : #|` e| = #|` e `\ i|.+1 by rewrite (cardfsD1 i) iIe. rewrite eE big_ord_recr /= (big_fsetD1 i) //= addnC. apply: leq_add; last by apply: IH; rewrite -eC eE. rewrite leq_exp2l // leq_min geq_minr andbT. apply: leq_trans (geq_minl _ _) _. apply: troot_le. rewrite -{2}iM -ltnS -eE -[#|`_|]prednK; last by rewrite eC. by apply: max_set_nat. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)