proposition: Lemma psi_cap_ge e1 e2 : phi (#|` e1 `|` e2|.+3) <= (psi e1 + psi e2).*2.*2 + 5.
proof: Proof. rewrite -(ler_nat (Num.NumDomain.clone _ int)) natrD. rewrite -!muln2 !natrM !mulr_natr -mulrnA natrD. set n := #|`_|. pose m := troot (n.+3). pose p := tmod (n.+3). pose l := m.-2. have mG2 : m >= 2 by rewrite root_delta_le. have pLm : p <= m. by rewrite leq_subLR -ltnS -[X in _ < X]addnS -deltaS -root_delta_lt ltnS. have nG : n >= delta l. rewrite -[n]/(n.+3.-2.-1) [n.+3]tmodE /l -/m. case: (m) mG2 => // [] [|] // m1 _. by rewrite deltaS deltaS /= !(addSn, addnS, subSS, subn0) -!addnA leq_addr. apply: le_trans (_ : ((psi_aux l `[0] + psi_aux l `[n]) *+ 4 + 5%:R <= _))%R; last first. rewrite lerD2r lerMn2r orFb. apply: le_trans (_ : psi_aux l e1 + psi_aux l e2 <= _)%R; last first. by apply: lerD; apply: psi_max. apply: le_trans (_ : psi_aux l (e1 `&` e2) + psi_aux l (e1 `|` e2) <= _)%R. apply: lerD; last by apply: psi_aux_card_le. apply: psi_aux_sub; rewrite sint0_set0. by apply/fsubsetP=> i; rewrite inE. rewrite /psi_aux. rewrite !natrD !addrA lerD // -!addrA lerD //. rewrite addrCA [X in (_ <= X)%R]addrCA lerD //. rewrite addrCA [X in (_ <= X)%R]addrCA lerD //. rewrite -!natrD ler_nat. rewrite [X in _ <= X + _](bigID (fun i => i \in e2)) /=. rewrite -!addnA leq_add //. rewrite leq_eqVlt; apply/orP; left; apply/eqP. by apply: eq_fbigl_cond => i; rewrite !inE /= andbT. rewrite [X in X <= _](bigID (fun i => i \in e2)) /=. rewrite addnC leq_add //. rewrite leq_eqVlt; apply/orP; left; apply/eqP. apply: eq_fbigl_cond => i; rewrite !inE /=. by case: (_ \in e2); rewrite ?(andbT, orbT, andbF, orbF). rewrite leq_eqVlt; apply/orP; left; apply/eqP. apply: eq_fbigl_cond => i; rewrite !inE /=. by case: (_ \in e2); rewrite /= ?(andbT, orbT, andbF, orbF). have pE : phi (n.+3) = ((m + p - 1) * 2 ^ m).+1. rewrite phi_modE -/m -/p -{1 4}[m]prednK 1?ltnW //. rewrite [(_ + p)%N]addSn mulSn [(2 ^ _ + _)%nat]addnC addnA addnK. by rewrite -subn1 -[(_ + _).+1]addn1 addnK. have pdE : ((phi (delta l))%:R = 1 + (l%:R - 1) * (2 ^ l)%:R :> int)%R. rewrite phi_deltaE natrB; last first. by case: (l) => // l1; rewrite mulSn addnCA leq_addr. by rewrite natrD /= mulrBl mul1r addrA -natrM. rewrite le_eqVlt; apply/orP; left; apply/eqP. rewrite psi_aux_sintE // psi_auxE_le. pose f i := 2 ^ minn (∇i) l. rewrite !(big_mkord _ f) big_ord0 addn0. have -> : [fset i in `[n] | l <= troot i] = [fset i in `[n] | delta l <= i]. by apply/fsetP=> i; rewrite !inE root_delta_le. have /(sint_sub n)-> : 0 <= delta l. by apply: (@delta_le 0). rewrite card_sint //. rewrite (_ : \sum_(_ <- _ | _) _ = phi (delta l)); last first. rewrite phiE. rewrite [LHS](eq_bigl (fun i => (i < n) && (∇i < l))); last first. move=> i; case: leqP; rewrite ?(andbT, andbF) // root_delta_lt. by move/(leq_trans)->. rewrite [RHS](eq_bigl (fun i : 'I_ _ => ((i : nat) \in (enum_fset `[n])))); last first. by move=> i; rewrite mem_sint (leq_trans (ltn_ord _)). elim: enum_fset (fset_uniq `[n]) => /= [_|a l1 IH /andP[aNIl lU]]. by rewrite big_nil big1. rewrite big_cons /= IH //; case: (boolP (a < n)) => aLn /=; last first. apply: eq_bigl => i; move: (ltn_ord i); rewrite inE; case: eqP => [->| //]. by move=> /leq_trans/(_ nG); rewrite (negPf aLn). case: leqP => aLl. apply: eq_bigl => i; move: (ltn_ord i); rewrite inE; case: eqP => [->| //]. by rewrite -root_delta_lt ltnNge aLl. rewrite root_delta_lt in aLl. rewrite [RHS](bigD1 (Ordinal aLl)); apply/eqP; last by rewrite inE eqxx. rewrite /= eqn_add2l; apply/eqP. apply: eq_bigl => i; rewrite !inE /= -val_eqE /=. by case: eqP (ltn_ord i) => [->|]; rewrite?(andbT, negPf aNIl). apply: etrans (_ : ((2 ^ l)%:R * (m.-1 + p)%:R - 1%:R) *+4 + 5%:R = _)%R; last first. congr (_ *+ _ + _)%R. rewrite -!subn1 ![in RHS](natrD, natrM, natrB) ?muln_gt0 ?expn_gt0 //. rewrite pdE !addrA addrK; set u := (2 ^ l)%:R%R. rewrite [(u - 1)%R]addrC -![in RHS]addrA [RHS]addrC; congr (_ - _)%R. rewrite -{2}[u]mul1r ![(u * _)%R]mulrC -![(-(_ * u))%R]mulNr -!mulrDl. congr (_ * _)%R. rewrite {u}!addrA addrAC addrK. rewrite -[(_ - _).+1]addn1 [in RHS]natrD !addrA addrK. rewrite -[n]/(n.+3.-2.-1) [n.+3]tmodE -/m -/p. rewrite -[in RHS](subnK mG2) ![in RHS](addnS, addn0) !deltaS !(subnS, subn0). rewrite ![in RHS](addnS, addSn) -!addnA [(delta _ + _)%nat]addnC addnK -/l. by rewrite ![in RHS]natrD !addrA subrK /l -(natrD _ 1%nat) -natrD. rewrite pE /l. case: (m) mG2 => // [] [|m1] //= _. rewrite addSn subn1 /=. rewrite (_ : 5%:R = 1 *+ 4 + 1)%R // addrA -mulrnDl. rewrite subrK -addn1 natrD; congr (_ + _)%R. rewrite -[in RHS]mulr_natr -!natrM [in RHS]mulnAC mulnC. congr (_ * _)%:R%R. by rewrite mulnC !expnS !mulnA. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)