proposition: Lemma psi_add n s e1 e2 : e1 `<=` `[n] -> n >= delta (s.-1) -> #|`e2| <= s -> psi (e1 `|` e2) - psi (e1) <= psi `[n + s] - psi `[n].
proof: Proof. move=> e1Sn. elim: s e2 => [e2 _|s IH e2 dLn Ce2]. rewrite leqn0 cardfs_eq0 => /eqP->. by rewrite fsetU0 subnn. have [->|[x xIe2]] := fset_0Vmem e2. by rewrite fsetU0 subnn. have dLn1 : delta (s.-1) <= n. apply: leq_trans dLn. by apply: delta_le; case: (s) => // s1 /=. pose e3 := e2 `\ x. have Ce3 : #|` e3| <= s. by move: Ce2; rewrite (cardfsD1 x) xIe2 ltnS. apply: leq_trans (leq_sub_add (psi (e1 `|` e3)) _ _) _. rewrite addnS psi_sintS. rewrite [X in _ <= X - _]addnC -addnBA; last first. by apply: psi_sint_leq; rewrite leq_addr. apply: leq_add; last by apply: IH. have [xIe1|xNIe1] := boolP (x \in e1). have -> : e1 `|` e2 = e1 `|` e3. apply/fsetP=> i; rewrite !inE. by case: eqP => // ->; rewrite xIe1. by rewrite subnn. have -> : e1 `|` e3 = (e1 `|` e2) `\ x. apply/fsetP=> i; rewrite !inE. case: eqP => // ->. by rewrite (negPf xNIe1). apply: psi_delta; last first. by rewrite !inE xIe2 orbT. rewrite -addnS. set t := s.+1. set g := troot (n + t). apply: leq_trans (_ : #|` e2 `|` (e1 `\` `[delta g])| <= _). apply: fsubset_leq_card. apply/fsubsetP=> i. rewrite !inE. by do 2 case: (_ \in _); rewrite ?(orbT, orbF). apply: leq_trans (_ : #|` e2| + #|` e1 `\` `[delta g]| <= _). by rewrite -cardfsUI leq_addr. apply: leq_trans (_ : t + #|` e1 `\` `[delta g]| <= _). by rewrite leq_add2r. apply: leq_trans (_ : t + #|` sint (delta g) n| <= _). rewrite leq_add2l. apply: fsubset_leq_card. apply/fsubsetP=> i. rewrite !(inE, mem_sint) /= -leqNgt => /andP[-> /(fsubsetP e1Sn)]. by rewrite mem_sint. rewrite card_sint. have [|E] := leqP n (delta g); last first. rewrite addnBA; last by apply: ltnW. rewrite leq_subLR addnC. by rewrite -ltnS -!addnS -deltaS addnS -root_delta_lt. move/eqP->; rewrite addn0. by rewrite root_delta_le deltaS leq_add2r. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)