psi.v

(******************************************************************************)
(*                                                                            *)
(*                                    PSI                                     *)
(*     psi n = the psi function                                               *)
(*                                                                            *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

From mathcomp Require Import all_ssreflect all_algebra finmap.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM;
                   GRing.smulr_closedN] : GRing.divring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedB;
 GRing.zmod_closedN] : GRing.divring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM;
                   GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedZ;
 GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.subring_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.divring_sdiv;
                   GRing.Pred.sdiv_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.divring_ring; GRing.Pred.subring_semi;
 GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
From hanoi Require Import extra triangular phi.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope fset_scope.
Open Scope nat_scope.


Section BigFSetAux.

Variable (R : Type) (idx : R) (op : Monoid.com_law idx).
Variable (I J : choiceType).

Lemma fsum_nat_const (e : {fset I}) a : \sum_(i <- e) a = #|` e| * a.R:Type
idx:R
op:Monoid.com_law idx
I, J:choiceType
e:{fset I}
a:nat
\sum_(i <- e) a = #|` e| * a
Proof.2 by rewrite big_const_seq count_predT iter_addn_0 mulnC. Qed.

Lemma diff_fset0_elem (e : {fset I}) : e != fset0 -> {i : I | i \in e}.56789
e != fset0 -> {i : I | i \in e}
Proof.e
by case: e => [] [|i l] iH //=; exists i; rewrite inE eqxx.
Qed.

(* Should be reworked  *)
Lemma eq_fbigmax (e : {fset I}) (F : I -> nat) :
  0 < #|`e| -> {i0 : I | i0 \in e /\ \max_(i <- e) F i = F i0}.56789F:I -> nat
0 < #|` e| ->
{i0 : I | i0 \in e /\ \max_(i <- e) F i = F i0}
Proof.14
have [n cI] := ubnP #|`e|; elim: n => // n IH e cI in e cI *.567817n:nat
IH:forall e : {fset I},
#|` e| < n ->
0 < #|` e| ->
{i0 : I | i0 \in e /\ \max_(i <- e) F i = F i0}
9cI:#|` e| < n.+1
18
rewrite cardfs_gt0 => /diff_fset0_elem[i iH].5678171e1f920i:I
iH:i \in e
{i0 : I | i0 \in e /\ \max_(i <- e) F i = F i0}
have [|H] := leqP #|`(e `\ i)| 0.24#|` e `\ i| <= 0 ->
{i0 : I | i0 \in e /\ \max_(i1 <- e) F i1 = F i0}
5678171e1f9202526H:0 < #|` e `\ i|
27
  rewrite leqn0 cardfs_eq0 => /eqP eZ.5678171e1f9202526eZ:e `\ i = fset0
27
2c
  exists i; split => //.33\max_(i <- e) F i = F i
2c
  rewrite (big_fsetD1 i) //= eZ big1_fset => [|j]; last by rewrite inE.33maxn (F i) 0 = F i
2c
  by apply/maxn_idPl.2e27
case: (IH (e `\ i)) => // [|j [jIe jH]].2e#|` e `\ i| < n
5678171e1f92025262fj:I
jIe:j \in e `\ i
jH:\max_(i <- e `\ i) F i = F j
27
  by move: cI; rewrite (cardfsD1 i) iH.4627
have [FiLFj|FjLFi] := leqP (F i) (F j).5678171e1f92025262f474849FiLFj:F i <= F j
27
5678171e1f92025262f474849FjLFi:F j < F i
27
  exists j; split => //.50j \in e
50\max_(i <- e) F i = F j
53
    by move: jIe; rewrite !inE => /andP[].505c
52
  rewrite (big_fsetD1 i) //= jH.50maxn (F i) (F j) = F j
52
  by apply/maxn_idPr.5427
exists i; split.54i \in e
5438
  by move: jIe; rewrite !inE => /andP[].5438
rewrite (big_fsetD1 i) //= jH.54maxn (F i) (F j) = F i
by apply/maxn_idPl/ltnW.
Qed.

Lemma big_fsetD1cond (a : I) (A : {fset I}) (P : pred I) (F : I -> R) : 
   a \in A -> P a ->
  \big[op/idx]_(i <- A | P i) F i = 
     op (F a) (\big[op/idx]_(i <- A `\ a | P i) F i).5678a:I
A:{fset I}
P:pred I
F:I -> R
a \in A ->
P a ->
\big[op/idx]_(i <- A | P i) F i =
op (F a) (\big[op/idx]_(i <- A `\ a | P i) F i)
Proof.75
move=> aA aP; rewrite (big_fsetIDcond _ (mem [fset a])).567878797a7baA:a \in A
aP:P a
op
  (\big[op/idx]_(i <- [fset x
                         | x in A
                         & mem [fset a] x] | P i) 
   F i)
  (\big[op/idx]_(i <- [fset x
                         | x in A
                         & ~~ mem [fset a] x] | P i)
      F i) =
op (F a) (\big[op/idx]_(i <- A `\ a | P i) F i)
congr (op _ _); last first.81\big[op/idx]_(i <- [fset x
                      | x in A
                      & ~~ mem [fset a] x] | P i) 
F i = \big[op/idx]_(i <- A `\ a | P i) F i
81\big[op/idx]_(i <- [fset x | x in A & mem [fset a] x] | 
P i) F i = F a
  by apply: eq_fbigl_cond => i; rewrite !inE /= [_ && (_ != _)]andbC.818b
rewrite (_ : [fset _ | _ in _ & _] = [fset a]).81\big[op/idx]_(i <- [fset a] | P i) F i = F a
81[fset H
   | H in mem_fin (fset_finpred A)
   & mem [fset a] H] = [fset a]
  rewrite big_seq_fsetE /= /index_enum /= -enumT enum_fset1 /=.81\big[op/idx]_(x <- [:: [` fset11 a]] | P (fsval x))
   F (fsval x) = F a
93
  by rewrite unlock /= aP Monoid.Theory.mulm1.8195
by apply/fsetP=> i; rewrite !inE /= andbC; case: eqP => //->.
Qed.

End BigFSetAux.

Section BigFSetAux.

Variable (R : Type) (idx : R) (op : Monoid.com_law idx).
Variable (I J : choiceType).

Lemma bigfmax_leqP (P : pred I) (m : nat) (e : {fset I}) (F : I -> nat) :
  reflect (forall i : I, i \in e -> P i -> F i <= m) 
          (\max_(i <- e | P i) F i <= m).56787am:nat
917
reflect (forall i : I, i \in e -> P i -> F i <= m)
  (\max_(i <- e | P i) F i <= m)
Proof.9e
apply: (iffP idP) => leFm => [i iIe Pi|].56787aa1917leFm:\max_(i <- e | P i) F i <= m
25iIe:i \in e
Pi:P i
F i <= m
56787aa1917leFm:forall i : I, i \in e -> P i -> F i <= m
\max_(i <- e | P i) F i <= m
  move: leFm.56787aa191725a9aa
\max_(i <- e | P i) F i <= m -> F i <= m
ac
  rewrite (big_fsetD1cond _ _ _ Pi) //= => /(leq_trans _)-> //.b4F i <= maxn (F i) (\max_(i <- e `\ i | P i) F i)
ac
  by apply: leq_maxl.aeb0
rewrite big_seq_cond.ae\max_(i <- e | (i \in e) && P i) F i <= m
elim/big_ind: _ => //= [m1 m2 m1Lm m2Ln | i /andP[]].56787aa1917afm1, m2:nat
m1Lm:m1 <= m
m2Ln:m2 <= m
maxn m1 m2 <= m
56787aa1917af25
i \in e -> P i -> F i <= m
  by rewrite geq_max m1Lm.cbcc
by apply: leFm.
Qed.

Lemma leq_bigfmax (e : {fset I}) (F : I -> nat) i :
   i \in e ->  F i <= \max_(i <- e) F i.567891725
i \in e -> F i <= \max_(i <- e) F i
Proof.d1
move=> iIe.567891725a9
F i <= \max_(i <- e) F i
have : i \in enum_fset e by [].d9d4
elim: enum_fset => //= a l IH.567891725a978l:seq I
IH:i \in l -> F i <= \max_(i <- l) F i
i \in a :: l -> F i <= \max_(i <- (a :: l)) F i
rewrite inE big_cons => /orP[/eqP<-|/IH H]; first by apply: leq_maxl.567891725a978e2e3H:F i <= \max_(i <- l) F i
F i <= maxn (F a) (\max_(j <- l) F j)
by apply: leq_trans H _; apply: leq_maxr.
Qed.

End BigFSetAux.

Section PsiDef.

Implicit Type e : {fset nat}.

Import Order.TTheory GRing.Theory Num.Theory.


Open Scope fset_scope.

Definition psi_aux l e : int :=
  ((2 ^ l).-1 + (\sum_(i <- e) 2 ^ (minn (troot i) l)))%:R - (l * 2 ^ l)%:R.

Notation "'ψ'' n" := (psi_aux n) (format "'ψ'' n", at level 0).

Lemma psi_aux_0_ge0 e :  (0 <= psi_aux 0 e)%R.e:{fset nat}
(0 <= ψ'(0) e)%R
Proof.ec by rewrite /psi_aux add0n mul0n subr0 (ler_nat _ 0). Qed.
Lemma psi_aux_sub l e1 e2 : e1 `<=` e2 -> (psi_aux l e1 <= psi_aux l e2)%R.l:nat
e1, e2:{fset nat}
e1 `<=` e2 -> (ψ'(l) e1 <= ψ'(l) e2)%R
Proof.f3
move=> e1Se2.f6f7e1Se2:e1 `<=` e2
(ψ'(l) e1 <= ψ'(l) e2)%R
apply: ler_sub => //.fd(((2 ^ l).-1 + \sum_(i <- e1) 2 ^ minn (∇i) l)%:R <=
 ((2 ^ l).-1 + \sum_(i <- e2) 2 ^ minn (∇i) l)%:R)%R
rewrite ler_nat.fd(2 ^ l).-1 + \sum_(i <- e1) 2 ^ minn (∇i) l <=
(2 ^ l).-1 + \sum_(i <- e2) 2 ^ minn (∇i) l
rewrite leq_add2l //.fd\sum_(i <- e1) 2 ^ minn (∇i) l <=
\sum_(i <- e2) 2 ^ minn (∇i) l
rewrite [X in _ <= X](bigID (fun i => i \in e1)) /=.fd\sum_(i <- e1) 2 ^ minn (∇i) l <=
\sum_(i <- e2 | i \in e1) 2 ^ minn (∇i) l +
\sum_(i <- e2 | i \notin e1) 2 ^ minn (∇i) l
suff iH : [fset x in e1 | xpredT x] =i [fset i in e2 | i \in e1].f6f7feiH:[fset x | x in e1 & true]
  =i [fset i | i in e2 & i \in e1]
10f
fd[fset x | x in e1 & true]
  =i [fset i | i in e2 & i \in e1]
  by rewrite (eq_fbigl_cond _ _ iH) /= leq_addr.fd117
move=> i; rewrite !inE /=.f6f7fei:nat_choiceType
(i \in [eta mem_seq e1]) && true =
(i \in [eta mem_seq e2]) && (i \in e1)
have /fsubsetP/(_ i) := e1Se2.11e(i \in e1 -> i \in e2) ->
(i \in [eta mem_seq e1]) && true =
(i \in [eta mem_seq e2]) && (i \in e1)
by case: (i \in e1) => [->//|]; rewrite andbF.
Qed.

Lemma psi_auxE_le l e :
  psi_aux l e = 
   (((2 ^ l * #|`[fset i in e | (l <= troot i)%nat]|.+1).-1 
    + (\sum_(i <- e | (troot i < l)%nat) 2 ^ troot i))%:R - (l * 2 ^ l)%:R)%R.f6ef
ψ'(l) e =
(((2 ^ l * #|` [fset i in e | (l <= ∇i)%N]|.+1).-1 +
  \sum_(i <- e | (∇i < l)%N) 2 ^ ∇i)%:R -
 (l * 2 ^ l)%:R)%R
Proof.126
rewrite /psi_aux.128(((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R)%R =
(((2 ^ l * #|` [fset i | i in e & (l <= ∇i)%N]|.+1).-1 +
  \sum_(i <- e | (∇i < l)%N) 2 ^ ∇i)%:R -
 (l * 2 ^ l)%:R)%R
congr (_%:R - _%:R)%R.128((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%N =
((2 ^ l * #|` [fset i | i in e & l <= ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i < l) 2 ^ ∇i)%N
rewrite (big_fsetID _ [pred i | l <= ∇i]) /=.128((2 ^ l).-1 +
 (\sum_(i <- [fset x | x in e & l <= ∇x])
     2 ^ minn (∇i) l +
  \sum_(i <- [fset x | x in e & ~~ (l <= ∇x)])
     2 ^ minn (∇i) l))%N =
((2 ^ l * #|` [fset i | i in e & l <= ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i < l) 2 ^ ∇i)%N
rewrite (@eq_fbigr _ _ _ _ _ _ _ (fun i => 2 ^ l)) /=; last first.128forall x : nat,
x \in [fset x0 | x0 in e & l <= ∇x0] ->
true -> 2 ^ minn (∇x) l = 2 ^ l
128((2 ^ l).-1 +
 (\sum_(i <- [fset x | x in e & l <= ∇x]) 2 ^ l +
  \sum_(i <- [fset x | x in e & ~~ (l <= ∇x)])
     2 ^ minn (∇i) l))%N =
((2 ^ l * #|` [fset i | i in e & l <= ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i < l) 2 ^ ∇i)%N
  by move=> i; rewrite !inE => /andP[_ /minn_idPr->].12813d
rewrite fsum_nat_const.128((2 ^ l).-1 +
 (#|` [fset x | x in e & l <= ∇x]| * 2 ^ l +
  \sum_(i <- [fset x | x in e & ~~ (l <= ∇x)])
     2 ^ minn (∇i) l))%N =
((2 ^ l * #|` [fset i | i in e & l <= ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i < l) 2 ^ ∇i)%N
rewrite (@eq_fbigr _ _ _ _ _ _ _  (fun i => 2 ^ (troot i))) /=; last first.128forall x : nat,
x \in [fset x0 | x0 in e & ~~ (l <= ∇x0)] ->
true -> 2 ^ minn (∇x) l = 2 ^ ∇x
128((2 ^ l).-1 +
 (#|` [fset x | x in e & l <= ∇x]| * 2 ^ l +
  \sum_(i <- [fset x | x in e & ~~ (l <= ∇x)]) 2 ^ ∇i))%N =
((2 ^ l * #|` [fset i | i in e & l <= ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i < l) 2 ^ ∇i)%N
  move=> i; rewrite !inE => /andP[_ H] _.f6efi:nat
H:~~ (l <= ∇i)
2 ^ minn (∇i) l = 2 ^ ∇i
149
  suff /minn_idPl-> : troot i <= l by [].14f∇i <= l
149
  by rewrite ltnW // ltnNge.12814b
rewrite addnA; congr (_ + _)%nat.128((2 ^ l).-1 + #|` [fset x | x in e & l <= ∇x]| * 2 ^ l)%N =
(2 ^ l * #|` [fset i | i in e & l <= ∇i]|.+1).-1
128\sum_(i <- [fset x | x in e & ~~ (l <= ∇x)]) 2 ^ ∇i =
\sum_(i <- e | ∇i < l) 2 ^ ∇i
  rewrite mulnS [_ ^ _ * #|`_|]mulnC.128((2 ^ l).-1 + #|` [fset x | x in e & l <= ∇x]| * 2 ^ l)%N =
(2 ^ l + #|` [fset i | i in e & l <= ∇i]| * 2 ^ l).-1
15e
  by case: (2 ^ l) (expn_gt0 2 l).128160
by apply: eq_fbigl_cond => i; rewrite !inE ltnNge andbT.
Qed.

Lemma psi_auxE_lt l e :
  psi_aux l e =
   (((2 ^ l * #|`[fset i in e | (l < troot i)%nat]|.+1).-1 
    + (\sum_(i <- e | (troot i <= l)%nat) 2 ^ troot i))%:R - (l * 2 ^ l)%:R)%R.128ψ'(l) e =
(((2 ^ l * #|` [fset i in e | (l < ∇i)%N]|.+1).-1 +
  \sum_(i <- e | (∇i <= l)%N) 2 ^ ∇i)%:R -
 (l * 2 ^ l)%:R)%R
Proof.169
rewrite /psi_aux.128(((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R)%R =
(((2 ^ l * #|` [fset i | i in e & (l < ∇i)%N]|.+1).-1 +
  \sum_(i <- e | (∇i <= l)%N) 2 ^ ∇i)%:R -
 (l * 2 ^ l)%:R)%R
congr (_%:R - _%:R)%R.128((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%N =
((2 ^ l * #|` [fset i | i in e & l < ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i <= l) 2 ^ ∇i)%N
rewrite (big_fsetID _ [pred i | l < troot i]) /=.128((2 ^ l).-1 +
 (\sum_(i <- [fset x | x in e & l < ∇x])
     2 ^ minn (∇i) l +
  \sum_(i <- [fset x | x in e & ~~ (l < ∇x)])
     2 ^ minn (∇i) l))%N =
((2 ^ l * #|` [fset i | i in e & l < ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i <= l) 2 ^ ∇i)%N
rewrite (@eq_fbigr _ _ _ _ _ _ _ (fun => 2 ^ l)) /=; last first.128forall x : nat,
x \in [fset x0 | x0 in e & l < ∇x0] ->
true -> 2 ^ minn (∇x) l = 2 ^ l
128((2 ^ l).-1 +
 (\sum_(i <- [fset x | x in e & l < ∇x]) 2 ^ l +
  \sum_(i <- [fset x | x in e & ~~ (l < ∇x)])
     2 ^ minn (∇i) l))%N =
((2 ^ l * #|` [fset i | i in e & l < ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i <= l) 2 ^ ∇i)%N
  by move=> i; rewrite !inE => /andP[_ /ltnW/minn_idPr ->].12817f
rewrite fsum_nat_const.128((2 ^ l).-1 +
 (#|` [fset x | x in e & l < ∇x]| * 2 ^ l +
  \sum_(i <- [fset x | x in e & ~~ (l < ∇x)])
     2 ^ minn (∇i) l))%N =
((2 ^ l * #|` [fset i | i in e & l < ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i <= l) 2 ^ ∇i)%N
rewrite (@eq_fbigr _ _ _ _ _ _ _ (fun i => 2 ^ troot i)) /=; last first.128forall x : nat,
x \in [fset x0 | x0 in e & ~~ (l < ∇x0)] ->
true -> 2 ^ minn (∇x) l = 2 ^ ∇x
128((2 ^ l).-1 +
 (#|` [fset x | x in e & l < ∇x]| * 2 ^ l +
  \sum_(i <- [fset x | x in e & ~~ (l < ∇x)]) 2 ^ ∇i))%N =
((2 ^ l * #|` [fset i | i in e & l < ∇i]|.+1).-1 +
 \sum_(i <- e | ∇i <= l) 2 ^ ∇i)%N
  move=> i; rewrite !inE /= => /andP[_ H] _.f6ef150H:~~ (l < ∇i)
152
18b
  suff /minn_idPl-> : troot i <= l by [].191156
18b
  by rewrite leqNgt.12818d
rewrite addnA; congr (_ + _)%nat.128((2 ^ l).-1 + #|` [fset x | x in e & l < ∇x]| * 2 ^ l)%N =
(2 ^ l * #|` [fset i | i in e & l < ∇i]|.+1).-1
128\sum_(i <- [fset x | x in e & ~~ (l < ∇x)]) 2 ^ ∇i =
\sum_(i <- e | ∇i <= l) 2 ^ ∇i
  rewrite mulnS [_ ^ _ * #|`_|]mulnC.128((2 ^ l).-1 + #|` [fset x | x in e & l < ∇x]| * 2 ^ l)%N =
(2 ^ l + #|` [fset i | i in e & l < ∇i]| * 2 ^ l).-1
19d
  by case: (2 ^ l) (expn_gt0 2 l).12819f
by apply: eq_fbigl_cond => i; rewrite !inE ltnNge andbT negbK.
Qed.

Definition psi_auxb e := (maxn #|`e| (\max_(i <- e) troot i)).+1.

Notation "'ψ_b' n" := (psi_auxb n) (format "'ψ_b' n", at level 0).

Lemma psi_aux_psib l e : psi_auxb e <= l -> (psi_aux l e <= 0)%R.128ψ_b(e) <= l -> (ψ'(l) e <= 0)%R
Proof.1a8
rewrite /psi_auxb; case: l => // l.eff6
maxn #|` e| (\max_(i <- e) ∇i) < l.+1 ->
(ψ'(l.+1) e <= 0)%R
rewrite ltnS /psi_aux geq_max => /andP[eLl maxLl].eff6eLl:#|` e| <= l
maxLl:\max_(i <- e) ∇i <= l
(((2 ^ l.+1).-1 + \sum_(i <- e) 2 ^ minn (∇i) l.+1)%:R -
 (l.+1 * 2 ^ l.+1)%:R <= 0)%R
rewrite mulSn -{2}[_ ^ _]prednK ?expn_gt0 // addSnnS.1b4(((2 ^ l.+1).-1 + \sum_(i <- e) 2 ^ minn (∇i) l.+1)%:R -
 ((2 ^ l.+1).-1 + (l * 2 ^ l.+1).+1)%:R <= 0)%R
rewrite !natrD [(_%:R + _)%R]addrC opprD addrA addrK.1b4((\sum_(i <- e) 2 ^ minn (∇i) l.+1)%:R -
 (l * 2 ^ l.+1).+1%:R <= 0)%R
rewrite subr_le0 ler_nat.1b4\sum_(i <- e) 2 ^ minn (∇i) l.+1 <= (l * 2 ^ l.+1).+1
apply: leq_trans (leqnSn _).1b4\sum_(i <- e) 2 ^ minn (∇i) l.+1 <= l * 2 ^ l.+1
apply: leq_trans (_ : #|`e| * 2 ^ l.+1 <= _); last first.1b4#|` e| * 2 ^ l.+1 <= l * 2 ^ l.+1
1b4\sum_(i <- e) 2 ^ minn (∇i) l.+1 <= #|` e| * 2 ^ l.+1
  by rewrite leq_mul2r eLl orbT.1b41ce
rewrite -fsum_nat_const.1b4\sum_(i <- e) 2 ^ minn (∇i) l.+1 <=
\sum_(i <- e) 2 ^ l.+1
apply: leq_sum => i iIe.eff61b51b611fiIe:true
2 ^ minn (∇i) l.+1 <= 2 ^ l.+1
apply: leq_pexp2l => //.1d9minn (∇i) l.+1 <= l.+1
by apply geq_minr.
Qed.

Definition rnz (z : int) := `|Num.max 0%R z|.

Lemma rnz_ler0 z : (z <= 0)%R -> rnz z = 0.z:int_numDomainType
(z <= 0)%R -> rnz z = 0
Proof.1e1 by move=>  zN; rewrite /rnz max_l. Qed.

Lemma rnz_ger0 z : (0 <= z)%R -> (z = (rnz z)%:R)%R.1e3(0 <= z)%R -> z = ((rnz z)%:R)%R
Proof.1e8 by move=>  zP; rewrite /rnz max_r // natz gez0_abs. Qed.

Lemma ler_rnz z : (z <= rnz z)%R.z:int_porderType
(z <= rnz z)%R
Proof.1ed by rewrite /rnz; case: ler0P => //= zP; rewrite gtz0_abs. Qed.

Lemma rnz_ler z1 z2 : (z1 <= z2)%R -> rnz z1 <= rnz z2.z1, z2:int_porderType
(z1 <= z2)%R -> rnz z1 <= rnz z2
Proof.1f4
rewrite /rnz; case: ler0P => // z1_gt0 z1Lz2; case: ler0P => //= [|z2_gt0].1f7z1_gt0:(0 < z1)%R
z1Lz2:(z1 <= z2)%R
(z2 <= 0)%R -> `|z1| <= 0
1f71fe1ffz2_gt0:(0 < z2)%R
`|z1| <= `|z2|
  by rewrite leNgt => /negP[]; apply: lt_le_trans z1Lz2.203205
by rewrite -lez_nat !gtz0_abs.
Qed.

Definition psi e := \max_(l < psi_auxb e) rnz (psi_aux l e).

Notation "'ψ' n" := (psi n) (format "'ψ' n", at level 0).

Lemma psiE_leq e n :
  psi_auxb e <= n -> psi e = \max_(l < n) rnz (psi_aux l e).ef1e
ψ_b(e) <= n -> ψ(e) = \max_(l < n) rnz (ψ'(l) e)
Proof.20a
move=> pLn.ef1epLn:ψ_b(e) <= n
ψ(e) = \max_(l < n) rnz (ψ'(l) e)
rewrite /psi.212\max_(l < ψ_b(e)) rnz (ψ'(l) e) =
\max_(l < n) rnz (ψ'(l) e)
rewrite (big_ord_widen_cond _ xpredT (fun i => rnz (psi_aux i e)) pLn).212\max_(i < n | true && (i < ψ_b(e))) rnz (ψ'(i) e) =
\max_(l < n) rnz (ψ'(l) e)
rewrite [RHS](bigID (fun i : 'I_n => i < psi_auxb e)) /=.212\max_(i < n | i < ψ_b(e)) rnz (ψ'(i) e) =
maxn (\max_(i < n | i < ψ_b(e)) rnz (ψ'(i) e))
  (\max_(i < n | ~~ (i < ψ_b(e))) rnz (ψ'(i) e))
rewrite [X in _ = maxn _ X]big1 ?maxn0 // => i.ef1e213i:'I_n
~~ (i < ψ_b(e)) -> rnz (ψ'(i) e) = 0
rewrite -leqNgt => /psi_aux_psib.224(ψ'(i) e <= 0)%R -> rnz (ψ'(i) e) = 0
exact: rnz_ler0.
Qed.

Lemma psi_max e l : (psi_aux l e <= (psi e)%:R)%R.1af(ψ'(l) e <= ψ(e)%:R)%R
Proof.22c
pose n := maxn (psi_auxb e) l.+1.eff6n:=maxn ψ_b(e) l.+1:nat
22e
have /psiE_leq-> : psi_auxb e <= n by apply: leq_maxl.233(ψ'(l) e <= (\max_(l < n) rnz (ψ'(l) e))%:R)%R
have O : l < n by apply: leq_maxr.eff6234O:l < n
238
have [/le_trans->//|/ltW/rnz_ger0->] := lerP (psi_aux l e) 0.23c(0 <= (\max_(l < n) rnz (ψ'(l) e))%:R)%R
23c((rnz (ψ'(l) e))%:R <= (\max_(l < n) rnz (ψ'(l) e))%:R)%R
  by rewrite (ler_nat _ 0).23c244
rewrite ler_nat.23crnz (ψ'(l) e) <= \max_(l < n) rnz (ψ'(l) e)
by rewrite (bigD1 (Ordinal O)) //= leq_maxl.
Qed.

Lemma psi_ler l e : 
  (((2 ^ l).-1 + \sum_(i <- e) 2 ^ (minn (troot i) l))%:R - (l * 2 ^ l)%:R 
      <= ((psi e)%:R : int))%R.128(((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R <= (ψ(e)%:R : int))%R
Proof.24d
have [/psi_aux_psib/le_trans->//|lLp] := leqP (psi_auxb e) l.128(0 <= ψ(e)%:R)%R
f6eflLp:l < ψ_b(e)
(((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R <= ψ(e)%:R)%R
  by rewrite (ler_nat _ 0).257259
rewrite [X in (_ <= X%:R)%R](bigD1 (Ordinal lLp)) //=.257(((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R <=
 (maxn (rnz (ψ'(l) e))
    (\max_(i < ψ_b(e) | i != Ordinal lLp)
        rnz (ψ'(i) e)))%:R)%R
apply: le_trans (ler_rnz _) _.257(rnz
   (((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R -
    (l * 2 ^ l)%:R) <=
 (maxn (rnz (ψ'(l) e))
    (\max_(i < ψ_b(e) | i != Ordinal lLp)
        rnz (ψ'(i) e)))%:R)%R
rewrite -natz ler_nat.257rnz
  (((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R -
   (l * 2 ^ l)%:R) <=
maxn (rnz (ψ'(l) e))
  (\max_(i < ψ_b(e) | i != Ordinal lLp) rnz (ψ'(i) e))
apply: leq_maxl.
Qed.

Lemma psiE e :  {l | ((psi e)%:R = psi_aux l e)%R}.ee{l : nat | (ψ(e)%:R)%R = ψ'(l) e}
Proof.26a
have [l] :  {l : 'I_(psi_auxb e) | psi e = rnz (psi_aux l e)}.ee{l : 'I_ψ_b(e) | ψ(e) = rnz (ψ'(l) e)}
efl:'I_ψ_b(e)
ψ(e) = rnz (ψ'(l) e) ->
{l : nat | (ψ(e)%:R)%R = ψ'(l) e}
  apply: eq_bigmax.ee0 < #|ordinal_finType ψ_b(e)|
272
  by rewrite card_ord.274276
rewrite /rnz; case: ler0P => [pG pE|pP ->]; last first.ef275pP:(0 < ψ'(l) e)%R
{l0 : nat | (`|ψ'(l) e|%:R)%R = ψ'(l0) e}
ef275pG:(ψ'(l) e <= 0)%R
pE:ψ(e) = `|0%R|
26c
  by exists l; rewrite natz gtz0_abs.28626c
by exists 0; apply/eqP; rewrite eq_le {1}pE psi_aux_0_ge0 psi_max.
Qed.

Lemma psi_sub e1 e2 : e1 `<=` e2 -> psi e1 <= psi e2.f7
e1 `<=` e2 -> ψ(e1) <= ψ(e2)
Proof.28d
move=> e1Se2.f7fe
ψ(e1) <= ψ(e2)
rewrite (psiE_leq (leq_maxl (psi_auxb e1) (psi_auxb e2))).295\max_(l < maxn ψ_b(e1) ψ_b(e2)) rnz (ψ'(l) e1) <=
ψ(e2)
rewrite (psiE_leq (leq_maxl (psi_auxb e2) (psi_auxb e1))).295\max_(l < maxn ψ_b(e1) ψ_b(e2)) rnz (ψ'(l) e1) <=
\max_(l < maxn ψ_b(e2) ψ_b(e1)) rnz (ψ'(l) e2)
rewrite maxnC.295\max_(l < maxn ψ_b(e2) ψ_b(e1)) rnz (ψ'(l) e1) <=
\max_(l < maxn ψ_b(e2) ψ_b(e1)) rnz (ψ'(l) e2)
elim/big_ind2: _ => // [x1 x2 y1 y2 x2Lx1 y2Ly1 | i _].f7fex1, x2, y1, y2:nat
x2Lx1:x2 <= x1
y2Ly1:y2 <= y1
maxn x2 y2 <= maxn x1 y1
f7fei:ordinal_finType (maxn ψ_b(e2) ψ_b(e1))
rnz (ψ'(i) e1) <= rnz (ψ'(i) e2)
  rewrite geq_max (leq_trans x2Lx1 (leq_maxl _ _)).2a6true && (y2 <= maxn x1 y1)
2ab
  by rewrite  (leq_trans y2Ly1 (leq_maxr _ _)).2ad2af
apply: rnz_ler.2ad(ψ'(i) e1 <= ψ'(i) e2)%R
by apply: psi_aux_sub.
Qed.

Lemma psi_aux_le_psi e1 e2 :
  (forall l, (psi_aux l e1 <= psi_aux l e2)%R) -> psi e1 <= psi e2.28f(forall l : nat, (ψ'(l) e1 <= ψ'(l) e2)%R) ->
ψ(e1) <= ψ(e2)
Proof.2bc
move=> H.f7H:forall l : nat, (ψ'(l) e1 <= ψ'(l) e2)%R
296
pose e := maxn (psi_auxb e1) (psi_auxb e2).f72c4e:=maxn ψ_b(e1) ψ_b(e2):nat
296
rewrite (psiE_leq (leq_maxl _ _ : _ <= e)).2c8\max_(l < e) rnz (ψ'(l) e1) <= ψ(e2)
rewrite (psiE_leq (leq_maxr _ _ : _ <= e)).2c8\max_(l < e) rnz (ψ'(l) e1) <=
\max_(l < e) rnz (ψ'(l) e2)
elim: e => [|e IH]; first by rewrite !big_ord0.f72c4e:nat
IH:\max_(l < e) rnz (ψ'(l) e1) <=
\max_(l < e) rnz (ψ'(l) e2)
\max_(l < e.+1) rnz (ψ'(l) e1) <=
\max_(l < e.+1) rnz (ψ'(l) e2)
by rewrite !big_ord_recr /= geq_max !leq_max IH /= rnz_ler // orbT.
Qed.

Lemma psi_auxb_sint n : psi_auxb `[n] = n.+1.1e
ψ_b(`[n]) = n.+1
Proof.2da
congr (_.+1).2dcmaxn #|` `[n]| (\max_(i <- `[n]) ∇i) = n
rewrite /psi_auxb.2e0
rewrite card_sint ?geq_minr // subn0.2dcmaxn n (\max_(i <- `[n]) ∇i) = n
apply/eqP.2dcmaxn n (\max_(i <- `[n]) ∇i) == n
rewrite eqn_leq leq_maxl andbT geq_max leqnn andTb.2dc\max_(i <- `[n]) ∇i <= n
apply/bigfmax_leqP => i; rewrite mem_sint /= => iLn _.1e11fiLn:i < n
∇i <= n
by apply: leq_trans (leq_rootnn _) (ltnW _).
Qed.

Lemma psi_aux_sintE n l :
  psi_aux l `[n] = 
  (((2 ^ l).-1 + \sum_(0 <= i <  n) 2 ^ minn (∇i) l)%:R -
   (l * 2 ^ l)%:R)%R.n, l:nat
ψ'(l) `[n] =
(((2 ^ l).-1 + \sum_(0 <= i < n) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R)%R
Proof.2f7
congr ((_ + _)%:R - _%:R)%R.2f9\sum_(i <- `[n]) 2 ^ minn (∇i) l =
\sum_(0 <= i < n) 2 ^ minn (∇i) l
elim: n => [|n IH]; first by rewrite sint0_set0 /= big_nil.l, n:nat
IH:\sum_(i <- `[n]) 2 ^ minn (∇i) l =
\sum_(0 <= i < n) 2 ^ minn (∇i) l
\sum_(i <- `[n.+1]) 2 ^ minn (∇i) l =
\sum_(0 <= i < n.+1) 2 ^ minn (∇i) l
rewrite (big_fsetD1 n) /=; last by rewrite mem_sint andTb.304(2 ^ minn (∇n) l +
 \sum_(i <- `[n.+1] `\ n) 2 ^ minn (∇i) l)%N =
\sum_(0 <= i < n.+1) 2 ^ minn (∇i) l
by rewrite sintSr IH !big_mkord big_ord_recr /= addnC.
Qed.

Lemma psi_auxb_set0 : psi_auxb fset0 = 1.ψ_b(fset0) = 1
Proof.30d by rewrite /psi_auxb cardfs0 max0n big_seq_cond big1. Qed.

Lemma  psi_set0 : psi fset0 = 0.ψ(fset0) = 0
Proof.312
rewrite /psi psi_auxb_set0.\max_(l < 1) rnz (ψ'(l) fset0) = 0
rewrite !big_ord_recr /= big_ord0 /= max0n.rnz (ψ'(0) fset0) = 0
by rewrite /psi_aux /= big_seq_cond big1.
Qed.

Lemma psi_eq0 e : (psi e == 0) = (e == fset0).ee(ψ(e) == 0) = (e == fset0)
Proof.31f
have [->|[x]] := fset_0Vmem e; first by rewrite psi_set0 !eqxx.efx:nat_choiceType
x \in e -> (ψ(e) == 0) = (e == fset0)
have [->|_] := e =P fset0; first by rewrite inE.326x \in e -> (ψ(e) == 0) = false
move=> xIe.ef327xIe:x \in e
(ψ(e) == 0) = false
suff : psi e > 0 by case: psi.3300 < ψ(e)
rewrite -(ltr_nat int_numDomainType).330(0%:R < ψ(e)%:R)%R
apply: lt_le_trans (psi_max _ 0).330(0%:R < ψ'(0) e)%R
by rewrite /psi_aux add0n subr0 ltr_nat (big_fsetD1 x).
Qed.

Lemma  psi_sint0 : psi `[0] = 0.ψ(`[0]) = 0
Proof.340 by rewrite sint0_set0 psi_set0. Qed.

Lemma  psi_sint1 : psi `[1] = 1.ψ(`[1]) = 1
Proof.345
rewrite /psi psi_auxb_sint.\max_(l < 2) rnz (ψ'(l) `[1]) = 1
rewrite -(big_mkord xpredT (fun l => rnz (psi_aux l _))).\max_(0 <= i < 2) rnz (ψ'(i) `[1]) = 1
pose f l := 
    rnz (((2 ^ l).-1 + \sum_(0 <= i <  1) 2 ^ minn (∇i) l)%:R -
         (l * 2 ^ l)%:R).f:=fun l : nat =>
rnz
  (((2 ^ l).-1 + \sum_(0 <= i < 1) 2 ^ minn (∇i) l)%:R -
   (l * 2 ^ l)%:R):nat -> nat
350
rewrite (eq_bigr f) => [|i _]; last by rewrite psi_aux_sintE.354\max_(0 <= i < 2) f i = 1
by rewrite /f /= unlock.
Qed.

Lemma  psi_sint2 : psi `[2] = 2.ψ(`[2]) = 2
Proof.35b
rewrite /psi psi_auxb_sint.\max_(l < 3) rnz (ψ'(l) `[2]) = 2
rewrite -(big_mkord xpredT (fun l => rnz (psi_aux l _))).\max_(0 <= i < 3) rnz (ψ'(i) `[2]) = 2
pose f l := 
    rnz (((2 ^ l).-1 + \sum_(0 <= i <  2) 2 ^ minn (∇i) l)%:R -
         (l * 2 ^ l)%:R).f:=fun l : nat =>
rnz
  (((2 ^ l).-1 + \sum_(0 <= i < 2) 2 ^ minn (∇i) l)%:R -
   (l * 2 ^ l)%:R):nat -> nat
366
rewrite (eq_bigr f) => [|i _]; last by rewrite psi_aux_sintE.36a\max_(0 <= i < 3) f i = 2
by rewrite /f /= unlock.
Qed.

Lemma  psi_sint3 : psi `[3] = 4.ψ(`[3]) = 4
Proof.371
rewrite /psi psi_auxb_sint.\max_(l < 4) rnz (ψ'(l) `[3]) = 4
rewrite -(big_mkord xpredT (fun l => rnz (psi_aux l _))).\max_(0 <= i < 4) rnz (ψ'(i) `[3]) = 4
pose f l := 
    rnz (((2 ^ l).-1 + \sum_(0 <= i <  3) 2 ^ minn (∇i) l)%:R -
         (l * 2 ^ l)%:R).f:=fun l : nat =>
rnz
  (((2 ^ l).-1 + \sum_(0 <= i < 3) 2 ^ minn (∇i) l)%:R -
   (l * 2 ^ l)%:R):nat -> nat
37c
rewrite (eq_bigr f) => [|i _]; last by rewrite psi_aux_sintE.380\max_(0 <= i < 4) f i = 4
by rewrite /f /= unlock.
Qed.

Lemma psi_aux_incr n l :
  l < (troot n).-1 -> (psi_aux l `[n] <= psi_aux l.+1 `[n])%R.2f9l < (∇n).-1 -> (ψ'(l) `[n] <= ψ'(l.+1) `[n])%R
Proof.387
move=> lLr.2falLr:l < (∇n).-1
(ψ'(l) `[n] <= ψ'(l.+1) `[n])%R
have dlLn : delta l.+2 <= n.38eΔl.+2 <= n
2fa38fdlLn:Δl.+2 <= n
390
  rewrite -root_delta_le -subn_gt0.38e0 < ∇n - l.+1
395
  by rewrite -[l.+1]addn1 addnC subnDA subn_gt0 subn1.397390
rewrite psi_auxE_lt psi_auxE_le.397(((2 ^ l * #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 +
  \sum_(i <- `[n] | (∇i <= l)%N) 2 ^ ∇i)%:R -
 (l * 2 ^ l)%:R <=
 ((2 ^ l.+1 *
   #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 +
  \sum_(i <- `[n] | (∇i < l.+1)%N) 2 ^ ∇i)%:R -
 (l.+1 * 2 ^ l.+1)%:R)%R
set s := \sum_(_ <- _ | _) _.2fa38f398s:=\sum_(H <- `[n] | ∇H <= l) 2 ^ ∇H:nat
(((2 ^ l * #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 +
  s)%:R - (l * 2 ^ l)%:R <=
 ((2 ^ l.+1 *
   #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 + s)%:R -
 (l.+1 * 2 ^ l.+1)%:R)%R
have -> : [fset i in `[n] | l < troot i] = [fset i in `[n] | delta l.+1 <= i].3a7[fset i | i in `[n] & l < ∇i] =
[fset i | i in `[n] & Δl.+1 <= i]
3a7(((2 ^ l *
   #|` [fset i | i in `[n] & (Δl.+1 <= i)%N]|.+1).-1 +
  s)%:R - (l * 2 ^ l)%:R <=
 ((2 ^ l.+1 *
   #|` [fset i | i in `[n] & (Δl.+1 <= i)%N]|.+1).-1 +
  s)%:R - (l.+1 * 2 ^ l.+1)%:R)%R
   by apply/fsetP => i; rewrite !inE root_delta_le.3a73b0
have /(sint_sub n)-> : 0 <= delta l.+1 by apply: delta_le (_ : 0 <= l.+1).3a7(((2 ^ l * #|` sint (Δl.+1) n|.+1).-1 + s)%:R -
 (l * 2 ^ l)%:R <=
 ((2 ^ l.+1 * #|` sint (Δl.+1) n|.+1).-1 + s)%:R -
 (l.+1 * 2 ^ l.+1)%:R)%R
rewrite card_sint //.3a7(((2 ^ l * (n - Δl.+1).+1).-1 + s)%:R - (l * 2 ^ l)%:R <=
 ((2 ^ l.+1 * (n - Δl.+1).+1).-1 + s)%:R -
 (l.+1 * 2 ^ l.+1)%:R)%R
set c := n - _.2fa38f3983a8c:=n - Δl.+1:nat
(((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R <=
 ((2 ^ l.+1 * c.+1).-1 + s)%:R - (l.+1 * 2 ^ l.+1)%:R)%R
rewrite expnS mulnAC [2 * _ * _]mulnC.3bf(((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R <=
 ((2 ^ l * (2 * c.+1)).-1 + s)%:R -
 (l.+1 * (2 * 2 ^ l))%:R)%R
rewrite mul2n mulnA muln2 -!addnn -[(_ + l.+1)%nat]addSnnS.3bf(((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R <=
 ((2 ^ l * (c.+1 + c.+1)).-1 + s)%:R -
 ((l.+2 + l) * 2 ^ l)%:R)%R
rewrite mulnDl mulnDr prednDr ?(muln_gt0, expn_gt0) //.3bf(((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R <=
 (2 ^ l * c.+1 + (2 ^ l * c.+1).-1 + s)%:R -
 (l.+2 * 2 ^ l + l * 2 ^ l)%:R)%R
set x := 2 ^ _ * _.2fa38f3983a83c0x:=2 ^ l * c.+1:nat
((x.-1 + s)%:R - (l * 2 ^ l)%:R <=
 (x + x.-1 + s)%:R - (l.+2 * 2 ^ l + l * 2 ^ l)%:R)%R
rewrite -[(_ + _ + s)%nat]addnA [(x + _)%nat]addnC.3d1((x.-1 + s)%:R - (l * 2 ^ l)%:R <=
 (x.-1 + s + x)%:R - (l.+2 * 2 ^ l + l * 2 ^ l)%:R)%R
rewrite [((_ + _ * _)%:R)%R]natrD opprD addrA ler_sub //.3d1((x.-1 + s)%:R <=
 (x.-1 + s + x)%:R - (l.+2 * 2 ^ l)%:R)%R
rewrite ler_subr_addr [((_ + x)%:R)%R]natrD ler_add //.3d1((l.+2 * 2 ^ l)%:R <= x%:R)%R
rewrite ler_nat.3d1l.+2 * 2 ^ l <= x
rewrite mulnC leq_mul2l.3d1(2 ^ l == 0) || (l.+1 < c.+1)
rewrite -subSn; last first.3d1Δl.+1 <= n
3d1(2 ^ l == 0) || (l.+1 < n.+1 - Δl.+1)
  apply: leq_trans (_ : delta l.+2 <= _); first by by apply: delta_le.3d1394
3ec
  by apply: leq_trans dlLn _.3d13ee
by rewrite ltn_subRL -addnS -deltaS (leq_trans dlLn) ?orbT.
Qed.

Lemma psi_aux_decr n l :
  (troot n).-1 <= l -> (psi_aux l.+1 `[n] <= psi_aux l `[n])%R.2f9(∇n).-1 <= l -> (ψ'(l.+1) `[n] <= ψ'(l) `[n])%R
Proof.3f6
move=> rLl.2farLl:(∇n).-1 <= l
(ψ'(l.+1) `[n] <= ψ'(l) `[n])%R
have dlLn : n < delta l.+2.3fdn < Δl.+2
2fa3fedlLn:n < Δl.+2
3ff
  rewrite ltnNge -root_delta_le -subn_gt0.3fd~~ (0 < ∇n - l.+1)
404
  by rewrite -[l.+1]addn1 addnC subnDA subn_gt0 subn1 -ltnNge.4063ff
rewrite psi_auxE_le.406(((2 ^ l.+1 *
   #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 +
  \sum_(i <- `[n] | (∇i < l.+1)%N) 2 ^ ∇i)%:R -
 (l.+1 * 2 ^ l.+1)%:R <= ψ'(l) `[n])%R
rewrite psi_auxE_lt.406(((2 ^ l.+1 *
   #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 +
  \sum_(i <- `[n] | (∇i < l.+1)%N) 2 ^ ∇i)%:R -
 (l.+1 * 2 ^ l.+1)%:R <=
 ((2 ^ l * #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 +
  \sum_(i <- `[n] | (∇i <= l)%N) 2 ^ ∇i)%:R -
 (l * 2 ^ l)%:R)%R
set s := \sum_(_ <- _ | _) _.2fa3fe407s:=\sum_(H <- `[n] | ∇H < l.+1) 2 ^ ∇H:nat
(((2 ^ l.+1 *
   #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 + s)%:R -
 (l.+1 * 2 ^ l.+1)%:R <=
 ((2 ^ l * #|` [fset i | i in `[n] & (l < ∇i)%N]|.+1).-1 +
  s)%:R - (l * 2 ^ l)%:R)%R
have -> : [fset i in `[n] | l < troot i] = 
          [fset i in `[n] | delta l.+1 <= i].41a3ad
41a(((2 ^ l.+1 *
   #|` [fset i | i in `[n] & (Δl.+1 <= i)%N]|.+1).-1 +
  s)%:R - (l.+1 * 2 ^ l.+1)%:R <=
 ((2 ^ l *
   #|` [fset i | i in `[n] & (Δl.+1 <= i)%N]|.+1).-1 +
  s)%:R - (l * 2 ^ l)%:R)%R
  by apply/fsetP => i; rewrite !inE root_delta_le.41a422
have /(sint_sub n)-> : 0 <= delta l.+1 by apply: delta_le (_ : 0 <= l.+1).41a(((2 ^ l.+1 * #|` sint (Δl.+1) n|.+1).-1 + s)%:R -
 (l.+1 * 2 ^ l.+1)%:R <=
 ((2 ^ l * #|` sint (Δl.+1) n|.+1).-1 + s)%:R -
 (l * 2 ^ l)%:R)%R
rewrite card_sint //.41a(((2 ^ l.+1 * (n - Δl.+1).+1).-1 + s)%:R -
 (l.+1 * 2 ^ l.+1)%:R <=
 ((2 ^ l * (n - Δl.+1).+1).-1 + s)%:R - (l * 2 ^ l)%:R)%R
set c := n - _.2fa3fe40741b3c0
(((2 ^ l.+1 * c.+1).-1 + s)%:R - (l.+1 * 2 ^ l.+1)%:R <=
 ((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R)%R
rewrite expnS mulnAC [2 * _ * _]mulnC.431(((2 ^ l * (2 * c.+1)).-1 + s)%:R -
 (l.+1 * (2 * 2 ^ l))%:R <=
 ((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R)%R
rewrite mul2n mulnA muln2 -!addnn -[(_ + l.+1)%nat]addSnnS.431(((2 ^ l * (c.+1 + c.+1)).-1 + s)%:R -
 ((l.+2 + l) * 2 ^ l)%:R <=
 ((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R)%R
rewrite mulnDl mulnDr prednDr ?(muln_gt0, expn_gt0) //.431((2 ^ l * c.+1 + (2 ^ l * c.+1).-1 + s)%:R -
 (l.+2 * 2 ^ l + l * 2 ^ l)%:R <=
 ((2 ^ l * c.+1).-1 + s)%:R - (l * 2 ^ l)%:R)%R
set x := 2 ^ _ * _.2fa3fe40741b3c03d2
((x + x.-1 + s)%:R - (l.+2 * 2 ^ l + l * 2 ^ l)%:R <=
 (x.-1 + s)%:R - (l * 2 ^ l)%:R)%R 
rewrite -[(_ + s)%nat]addnA [(x + _)%nat]addnC.442((x.-1 + s + x)%:R - (l.+2 * 2 ^ l + l * 2 ^ l)%:R <=
 (x.-1 + s)%:R - (l * 2 ^ l)%:R)%R
rewrite [((_ + _ * _)%:R)%R]natrD opprD addrA ler_sub //.442((x.-1 + s + x)%:R - (l.+2 * 2 ^ l)%:R <=
 (x.-1 + s)%:R)%R
rewrite ler_subl_addr [((_ + x)%:R)%R]natrD ler_add //.442(x%:R <= (l.+2 * 2 ^ l)%:R)%R
rewrite ler_nat.442x <= l.+2 * 2 ^ l
rewrite mulnC leq_mul2l.442(2 ^ l == 0) || (c < l.+2)
rewrite -[l.+2](addnK (delta l.+1)) addnC -deltaS.442(2 ^ l == 0) || (c < Δl.+2 - Δl.+1)
rewrite ltn_sub2r ?orbT // [X in _ < X]deltaS //.442Δl.+1 < Δl.+1 + l.+2
by rewrite addnS ltnS leq_addr.
Qed.

Lemma psi_aux_sint n : ((psi `[n])%:R)%R = psi_aux (troot n).-1 `[n].2dc(ψ(`[n])%:R)%R = ψ'((∇n).-1) `[n]
Proof.461
apply/eqP.2dc(ψ(`[n])%:R)%R == ψ'((∇n).-1) `[n]
rewrite eq_le psi_max andbT.2dc(ψ(`[n])%:R <= ψ'((∇n).-1) `[n])%R
case: (psiE `[n]) => l ->.2f9(ψ'(l) `[n] <= ψ'((∇n).-1) `[n])%R
have [E|E] := leqP (troot n).-1 l.2faE:(∇n).-1 <= l
470
2faE:l < (∇n).-1
470
  rewrite -(subnK E).474(ψ'(l - (∇n).-1 + (∇n).-1) `[n] <= ψ'((∇n).-1) `[n])%R
476
  elim: (_ - _) => [|k IH] //.2fa475k:nat
IH:(ψ'(k + (∇n).-1) `[n] <= ψ'((∇n).-1) `[n])%R
(ψ'(k.+1 + (∇n).-1) `[n] <= ψ'((∇n).-1) `[n])%R
476
  apply: le_trans IH.2fa475482
(ψ'(k.+1 + (∇n).-1) `[n] <= ψ'(k + (∇n).-1) `[n])%R
476
  rewrite addSn.488(ψ'((k + (∇n).-1).+1) `[n] <= ψ'(k + (∇n).-1) `[n])%R
476
  apply: psi_aux_decr => //.488(∇n).-1 <= k + (∇n).-1
476
  by rewrite leq_addl.478470
rewrite -(subKn (ltnW E)).478(ψ'((∇n).-1 - ((∇n).-1 - l)) `[n] <= ψ'((∇n).-1) `[n])%R
elim: (_ - l) => [|k IH].478(ψ'((∇n).-1 - 0) `[n] <= ψ'((∇n).-1) `[n])%R
2fa479482IH:(ψ'((∇n).-1 - k) `[n] <= ψ'((∇n).-1) `[n])%R
(ψ'((∇n).-1 - k.+1) `[n] <= ψ'((∇n).-1) `[n])%R
  by rewrite subn0.49f4a1
apply: le_trans IH.2fa479482
(ψ'((∇n).-1 - k.+1) `[n] <= ψ'((∇n).-1 - k) `[n])%R
rewrite subnS.4a8(ψ'(((∇n).-1 - k).-1) `[n] <= ψ'((∇n).-1 - k) `[n])%R
have [|E1] := leqP (troot n).-1 k.4a8(∇n).-1 <= k ->
(ψ'(((∇n).-1 - k).-1) `[n] <= ψ'((∇n).-1 - k) `[n])%R
2fa479482E1:k < (∇n).-1
4ad
  by rewrite -subn_eq0 => /eqP->.4b44ad
rewrite -{2}[_-_]prednK ?subn_gt0 //.4b4(ψ'(((∇n).-1 - k).-1) `[n] <=
 ψ'(((∇n).-1 - k).-1.+1) `[n])%R
apply: psi_aux_incr => //.4b4((∇n).-1 - k).-1 < (∇n).-1
case: _.-1 E1 => // u _; case: k => // k.2fa479u, k:nat
(u.+1 - k.+1).-1 < u.+1
apply: leq_trans (_ : u.+1.-1 < u.+1) => //.4c4(u.+1 - k.+1).-1 < u.+1.-1.+1
by rewrite ltnS -!subn1 leq_sub2r // leq_subr.
Qed.

(* This is 2.2 *)
Lemma psi_sint_phi n : (psi `[n]).*2 = (phi n.+1).-1.2dcψ(`[n]).*2 = ϕ(n.+1).-1
Proof.4cc
have [|nP] := leqP n 0; first by case: (n)=> //; rewrite psi_sint0.1enP:0 < n
4ce
apply/eqP; rewrite -(eqr_nat int_numDomainType).4d3(ψ(`[n]).*2%:R)%R == (ϕ(n.+1).-1%:R)%R
rewrite -muln2 natrM mulr_natr.4d3(ψ(`[n])%:R *+ 2)%R == (ϕ(n.+1).-1%:R)%R
rewrite psi_aux_sint // psi_auxE_lt.4d3((((2 ^ (∇n).-1 *
    #|` [fset i | i in `[n] & ((∇n).-1 < ∇i)%N]|.+1).-1 +
   \sum_(i <- `[n] | (∇i <= (∇n).-1)%N) 2 ^ ∇i)%:R -
  ((∇n).-1 * 2 ^ (∇n).-1)%:R) *+ 2)%R ==
(ϕ(n.+1).-1%:R)%R
rewrite (_ : [fset _ in _ | _] = [fset i in `[n] | delta (troot n) <= i]);
   last first.4d3[fset H
   | H in mem_fin (fset_finpred `[n])
   & (∇n).-1 < ∇H] = [fset i | i in `[n] & Δ(∇n) <= i]
4d3((((2 ^ (∇n).-1 *
    #|` [fset i | i in `[n] & (Δ(∇n) <= i)%N]|.+1).-1 +
   \sum_(i <- `[n] | (∇i <= (∇n).-1)%N) 2 ^ ∇i)%:R -
  ((∇n).-1 * 2 ^ (∇n).-1)%:R) *+ 2)%R ==
(ϕ(n.+1).-1%:R)%R
  apply/fsetP=> i; rewrite !inE; congr (_ && _).1e4d411f
((∇n).-1 < ∇i) = (Δ(∇n) <= i)
4e5
  by rewrite prednK ?troot_gt0 // root_delta_le.4d34e7
rewrite sint_sub ?delta_gt0 ?troot_gt0 // card_sint //.4d3((((2 ^ (∇n).-1 * (n - Δ(∇n)).+1).-1 +
   \sum_(i <- `[n] | (∇i <= (∇n).-1)%N) 2 ^ ∇i)%:R -
  ((∇n).-1 * 2 ^ (∇n).-1)%:R) *+ 2)%R ==
(ϕ(n.+1).-1%:R)%R
rewrite (_ : \sum_(i <- _ | _) _  = phi (delta (troot n))); last first.4d3\sum_(i <- `[n] | ∇i <= (∇n).-1) 2 ^ ∇i = ϕ(Δ(∇n))
4d3((((2 ^ (∇n).-1 * (n - Δ(∇n)).+1).-1 + ϕ(Δ(∇n)))%:R -
  ((∇n).-1 * 2 ^ (∇n).-1)%:R) *+ 2)%R ==
(ϕ(n.+1).-1%:R)%R
  rewrite phiE.4d3\sum_(i <- `[n] | ∇i <= (∇n).-1) 2 ^ ∇i =
\sum_(i < Δ(∇n)) 2 ^ ∇i
4f8
  rewrite [RHS](eq_bigl 
        (fun i : 'I_ _ => (i : nat) \in (enum_fset `[n]))); last first.4d3xpredT =1 (fun i : 'I_(Δ(∇n)) => i \in `[n])
4d3\sum_(i <- `[n] | ∇i <= (∇n).-1) 2 ^ ∇i =
\sum_(i < Δ(∇n) | i \in `[n]) 2 ^ ∇i
4f9
    move=> i.1e4d4i:'I_(Δ(∇n))
true = (i \in `[n])
503
    by rewrite mem_sint leq0n (leq_trans (ltn_ord _)) // delta_root_le.4d3505
4f8
  elim: enum_fset (fset_uniq `[n]) => /= [_|a l IH /andP[aNIl lU]].4d3\sum_(i <- [::] | ∇i <= (∇n).-1) 2 ^ ∇i =
\sum_(i < Δ(∇n) | i \in [::]) 2 ^ ∇i
1e4d4al:seq nat
IH:uniq l ->
\sum_(i <- l | ∇i <= (∇n).-1) 2 ^ ∇i =
\sum_(i < Δ(∇n) | i \in l) 2 ^ ∇i
aNIl:a \notin l
lU:uniq l
\sum_(i <- (a :: l) | ∇i <= (∇n).-1) 2 ^ ∇i =
\sum_(i < Δ(∇n) | i \in a :: l) 2 ^ ∇i
4f9
    by rewrite big_nil big1.51551a
4f8
  rewrite big_cons /= IH //; case: leqP => aLb; last first.1e4d4a516517518519aLb:(∇n).-1 < ∇a
\sum_(i < Δ(∇n) | i \in l) 2 ^ ∇i =
\sum_(i < Δ(∇n) | i \in a :: l) 2 ^ ∇i
1e4d4a516517518519aLb:∇a <= (∇n).-1
(2 ^ ∇a + \sum_(i < Δ(∇n) | i \in l) 2 ^ ∇i)%N =
\sum_(i < Δ(∇n) | i \in a :: l) 2 ^ ∇i
4f9
    rewrite prednK ?troot_gt0 // in aLb.1e4d4a516517518519aLb:∇n <= ∇a
523
524
    apply: eq_bigl => i; rewrite inE eqn_leq [a <= i]leqNgt.1e4d4a51651751851952d50a
(i \in l) = (i <= a) && ~~ (i < a) || (i \in l)
524
    by rewrite (leq_trans (ltn_ord i)) ?andbF // -root_delta_le.526528
4f8
  have aLn : a < Δ(∇n).526a < Δ(∇n)
1e4d4a516517518519527aLn:a < Δ(∇n)
528
4f9
    by rewrite -root_delta_lt -[troot n]prednK // troot_gt0.53c528
4f8
  rewrite [RHS](bigD1 (Ordinal aLn)) ?(inE, eqxx) //=.53c(2 ^ ∇a + \sum_(i < Δ(∇n) | i \in l) 2 ^ ∇i)%N =
(2 ^ ∇a +
 \sum_(i < Δ(∇n) | (i \in a :: l) &&
                   (i != Ordinal aLn)) 2 ^ ∇i)%N
4f8
  congr ((_ + _)%nat).53c\sum_(i < Δ(∇n) | i \in l) 2 ^ ∇i =
\sum_(i < Δ(∇n) | (i \in a :: l) && (i != Ordinal aLn))
   2 ^ ∇i
4f8
  apply: eq_bigl => i; rewrite inE -val_eqE /=.1e4d4a51651751851952753d50a
(i \in l) = ((i == a) || (i \in l)) && (i != a)
4f8
  by case: (_ =P _); rewrite ?andbT // => ->; rewrite (negPf aNIl).4d34fa
set m := troot n.1e4d4m:=∇n:nat
((((2 ^ m.-1 * (n - Δm).+1).-1 + ϕ(Δm))%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
rewrite -[n - _]/(tmod n).554((((2 ^ m.-1 * (tmod n).+1).-1 + ϕ(Δm))%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
set p := tmod n.1e4d4555p:=tmod n:nat
((((2 ^ m.-1 * p.+1).-1 + ϕ(Δm))%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
rewrite phi_deltaE.55e((((2 ^ m.-1 * p.+1).-1 + (1 + m * 2 ^ m - 2 ^ m))%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
(* taking care of  m * 2 ^ m - 2 ^ m *)
rewrite -{2}[m]prednK ?troot_gt0 //.55e((((2 ^ m.-1 * p.+1).-1 +
   (1 + m.-1.+1 * 2 ^ m - 2 ^ m))%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
rewrite mulSn addnCA [(2 ^ _ + _)%nat]addnC addnK add1n.55e((((2 ^ m.-1 * p.+1).-1 + (m.-1 * 2 ^ m).+1)%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
rewrite addnS -addSn prednK; last first.55e0 < 2 ^ m.-1 * p.+1
55e(((2 ^ m.-1 * p.+1 + m.-1 * 2 ^ m)%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
  by rewrite muln_gt0 expn_gt0.55e573 
(* taking care of m.-1 * 2 ^ m - m.-1 * 2 ^ m.-1 *)
rewrite -{3}[m]prednK ?troot_gt0 //.55e(((2 ^ m.-1 * p.+1 + m.-1 * 2 ^ m.-1.+1)%:R -
  (m.-1 * 2 ^ m.-1)%:R) *+ 2)%R == (ϕ(n.+1).-1%:R)%R
rewrite expnS mul2n -addnn mulnDr addnA natrD addrK.55e((2 ^ m.-1 * p.+1 + m.-1 * 2 ^ m.-1)%:R *+ 2)%R ==
(ϕ(n.+1).-1%:R)%R
rewrite mulnC -mulnDl addSnnS prednK ?troot_gt0 //.55e(((p + m) * 2 ^ m.-1)%:R *+ 2)%R == (ϕ(n.+1).-1%:R)%R
rewrite -mulr_natr -natrM muln2 eqr_nat.55e((p + m) * 2 ^ m.-1).*2 == ϕ(n.+1).-1
rewrite phi_modSE -/m -/p.55e((p + m) * 2 ^ m.-1).*2 == (1 + (m + p) * 2 ^ m).-1
rewrite add1n -pred_Sn addnC -{4}[m]prednK ?troot_gt0 //.55e((m + p) * 2 ^ m.-1).*2 == (m + p) * 2 ^ m.-1.+1
by rewrite expnS mulnCA mul2n.
Qed.

Lemma psi_sint_leq a b : a <= b -> psi `[a] <= psi `[b].a, b:nat
a <= b -> ψ(`[a]) <= ψ(`[b])
Proof.590
move=> aLb; apply: psi_sub; apply/fsubsetP=> i.593aLb:a <= b
11f
i \in `[a] -> i \in `[b]
by rewrite !mem_sint /= => iLa; apply: leq_trans aLb.
Qed.

Lemma psi_sintS n : (psi `[n.+1] = psi `[n] + 2 ^ (troot n.+1).-1)%nat.2dcψ(`[n.+1]) = (ψ(`[n]) + 2 ^ (∇n.+1).-1)%N
Proof.59d
have F : 0 < phi n.+1 by apply: phi_le (_ : 1 <= _).1eF:0 < ϕ(n.+1)
59f
apply: double_inj; rewrite doubleD.5a4ψ(`[n.+1]).*2 = (ψ(`[n]).*2 + (2 ^ (∇n.+1).-1).*2)%N
rewrite !psi_sint_phi //.5a4ϕ(n.+2).-1 = (ϕ(n.+1).-1 + (2 ^ (∇n.+1).-1).*2)%N
rewrite -mul2n -expnS prednK ?troot_gt0 //.5a4ϕ(n.+2).-1 = (ϕ(n.+1).-1 + 2 ^ ∇n.+1)%N
by rewrite phiE big_ord_recr -phiE prednDl.
Qed.

(* This is 2.2 *)
Lemma psi_leD a b : psi `[a + b] <= (psi `[a]).*2 + 2 ^ (b.-1).592ψ(`[a + b]) <= ψ(`[a]).*2 + 2 ^ b.-1
Proof.5b3
case: b => [|b]; first by rewrite addn0 -addnn -addnA leq_addr.592ψ(`[a + b.+1]) <= ψ(`[a]).*2 + 2 ^ b.+1.-1
rewrite -leq_double doubleD [_.+1.-1]/=.592ψ(`[a + b.+1]).*2 <= (ψ(`[a]).*2).*2 + (2 ^ b).*2
rewrite !psi_sint_phi -addSn -ltnS prednK ?phi_gt0 //.592ϕ(a.+1 + b.+1) <= ((ϕ(a.+1).-1).*2 + (2 ^ b).*2).+1
apply: leq_trans (phi_leD _ _) _.592ϕ(a.+1).*2 + (2 ^ b.+1).-1 <=
((ϕ(a.+1).-1).*2 + (2 ^ b).*2).+1
rewrite -{1}[phi (a.+1)]prednK ?phi_gt0 // doubleS.592(ϕ(a.+1).-1).*2.+2 + (2 ^ b.+1).-1 <=
((ϕ(a.+1).-1).*2 + (2 ^ b).*2).+1
by rewrite expnS mul2n -prednDr ?double_gt0 ?expn_gt0.
Qed.

(* This is 2.3 *)
Lemma psi_SS_le n : psi `[n.+2] >= 2 ^(troot n).+1.2dc2 ^ (∇n).+1 <= ψ(`[n.+2])
Proof.5cc
case: n => [|n]; first by rewrite psi_sint2.2dc2 ^ (∇n.+1).+1 <= ψ(`[n.+3])
have /psi_sint_leq/(leq_trans _)->// : (delta (troot n.+1)).+2 <= n.+3.2dc(Δ(∇n.+1)).+1 < n.+3
2dc2 ^ (∇n.+1).+1 <= ψ(`[(Δ(∇n.+1)).+2])
  by rewrite !ltnS -root_delta_le.2dc5da
set s := troot _.1es:=∇n.+1:nat
2 ^ s.+1 <= ψ(`[(Δs).+2])
have [|tLs] := leqP s 1.5e1s <= 1 -> 2 ^ s.+1 <= ψ(`[(Δs).+2])
1e5e2tLs:1 < s
5e3
  case: s => [|[|]] //; first by rewrite psi_sint2 ?(leq_trans _ thLN).2dc0 < 1 -> 2 ^ 2 <= ψ(`[(Δ1).+2])
5e8
  by rewrite psi_sint3.5ea5e3
rewrite -leq_double psi_sint_phi phi_modSE.5ea(2 ^ s.+1).*2 <=
(1 + (∇(Δs).+2 + tmod (Δs).+2) * 2 ^ ∇(Δs).+2).-1
have tE : troot (delta s).+2 = s.5ea∇(Δs).+2 = s
1e5e25ebtE:∇(Δs).+2 = s
5f6
  by apply/eqP; rewrite trootE deltaS ltnW //= -addn2 addSnnS leq_add2l.5fd5f6
rewrite tE.5fd(2 ^ s.+1).*2 <= (1 + (s + tmod (Δs).+2) * 2 ^ s).-1
have->: tmod (delta s).+2 = 2 by rewrite /tmod tE -addn2 addnC addnK.5fd(2 ^ s.+1).*2 <= (1 + (s + 2) * 2 ^ s).-1
by rewrite -mul2n expnS mulnA /= leq_mul2r (leq_add2r 2 2) tLs orbT.
Qed.

Lemma psi_aux0_sint n : psi_aux 0 `[n] = n.2dcψ'(0) `[n] = n
Proof.60b
rewrite /psi_aux add0n subr0.2dc((\sum_(i <- `[n]) 2 ^ minn (∇i) 0)%:R)%R = n
apply/eqP; rewrite -natz eqr_nat; apply/eqP.2dc\sum_(i <- `[n]) 2 ^ minn (∇i) 0 = n
rewrite (eq_bigr (fun => 1)) => [|i _].2dc\sum_(i <- `[n]) 1 = n
1e11f
2 ^ minn (∇i) 0 = 1
  by rewrite fsum_nat_const card_sint // subn0 muln1.61d61e
by rewrite minn0.
Qed.

(* This is 2.4.1 *)
Lemma psi_sint_min n : n <= psi `[n].2dcn <= ψ(`[n])
Proof.623
rewrite -(ler_nat int_numDomainType).2dc(n%:R <= ψ(`[n])%:R)%R
rewrite natz -[X in (X <= _)%R]psi_aux0_sint.2dc(ψ'(0) `[n] <= ψ(`[n])%:R)%R
by apply: psi_max.
Qed.

Lemma sum_sint (F : nat -> nat) n : 
  \sum_(i <- `[n]) F i  = \sum_(i < n) F i.F:nat -> nat
1e
\sum_(i <- `[n]) F i = \sum_(i < n) F i
Proof.630
rewrite big_seq_cond.632\sum_(i <- `[n] | (i \in `[n]) && true) F i =
\sum_(i < n) F i
rewrite [LHS](eq_bigl (fun i => (i < n))); last first.632(fun i : nat => (i \in `[n]) && true) =1
(fun i : nat => i < n)
632\sum_(i <- `[n] | i < n) F i = \sum_(i < n) F i
  by move=> i; rewrite mem_sint andbT.632640
rewrite [RHS](eq_bigl 
        (fun i : 'I_ _ => ((i : nat) \in (enum_fset `[n])))); last first.632xpredT =1 (fun i : 'I_n => i \in `[n])
632\sum_(i <- `[n] | i < n) F i =
\sum_(i < n | i \in `[n]) F i
  by move=> i; rewrite mem_sint ltn_ord.63264a
elim: enum_fset (fset_uniq `[n]) => /= [_|a l IH /andP[aNIl lU]].632\sum_(i <- [::] | i < n) F i =
\sum_(i < n | i \in [::]) F i
633n, a:nat
516IH:uniq l ->
\sum_(i <- l | i < n) F i =
\sum_(i < n | i \in l) F i
518519
\sum_(i <- (a :: l) | i < n) F i =
\sum_(i < n | i \in a :: l) F i
  by rewrite big_nil big1.654657
rewrite big_cons /= IH //; case: (boolP (a < n)) => aLn; last first.633655516656518519aLn:~~ (a < n)
\sum_(i < n | i \in l) F i =
\sum_(i < n | i \in a :: l) F i
633655516656518519aLn:a < n
(F a + \sum_(i < n | i \in l) F i)%N =
\sum_(i < n | i \in a :: l) F i
  apply: eq_bigl => i; move: (ltn_ord i); rewrite inE; case: eqP => [->| //].63365551665651851965f225
a < n -> (a \in l) = true || (a \in l)
661
  by rewrite (negPf aLn).663665
rewrite [RHS](bigD1 (Ordinal aLn)) ?(inE, eqxx) //=.663(F a + \sum_(i < n | i \in l) F i)%N =
(F a +
 \sum_(i < n | (i \in a :: l) && (i != Ordinal aLn))
    F i)%N
congr ((_ + _)%nat).663\sum_(i < n | i \in l) F i =
\sum_(i < n | (i \in a :: l) && (i != Ordinal aLn))
   F i
apply: eq_bigl => i; rewrite inE -val_eqE /=.633655516656518519664225
54d
by case: (_ =P _); rewrite ?andbT // => ->; rewrite (negPf aNIl).
Qed.

Lemma max_set_nat (e : {fset nat}) : #|`e|.-1 <= \max_(i <- e) i.ee#|` e|.-1 <= \max_(i <- e) i
Proof.67b
have [n cI] := ubnP #|`e|; elim: n => // [] [|n] IH e cI in e cI *.IH:forall e,
#|` e| < 0 -> #|` e|.-1 <= \max_(i <- e) i
efcI:#|` e| < 1
67d
1eIH:forall e,
#|` e| < n.+1 -> #|` e|.-1 <= \max_(i <- e) i
efcI:#|` e| < n.+2
67d
  by move: cI; rewrite ltnS leqn0 => /eqP->.68767d
move: cI; rewrite leq_eqVlt => /orP[/eqP eC|]; last first.1e688ef
#|` e|.+1 < n.+2 -> #|` e|.-1 <= \max_(i <- e) i
1e688efeC:#|` e|.+1 = n.+2
67d
  by apply: IH.69467d
have /(eq_fbigmax id)[/= i [iIe iM]] : 0 < #|`e| by rewrite -ltnS eC.1e688ef695150a9iM:\max_(i <- e) i = i
67d
have  eE : #|` e| = #|` e `\ i|.+1 by rewrite (cardfsD1 i) iIe.1e688ef695150a969deE:#|` e| = #|` e `\ i|.+1
67d
have /IH H : #|`e `\ i| < n.+1 by rewrite -eE -ltnS eC.1e688ef695150a969d6a2H:#|` e `\ i|.-1 <= \max_(i <- e `\ i) i
67d
rewrite eE /=.6a6#|` e `\ i| <= \max_(i <- e) i
case eIE : (#|` e `\ i|) => [//|k].1e688ef695150a969d6a26a7482eIE:#|` e `\ i| = k.+1
k < \max_(i <- e) i
have /(eq_fbigmax id)[j []] : 0 < #|` e `\ i| by rewrite eIE.1e688ef695150a969d6a26a74826b0j:nat_choiceType
j \in e `\ i ->
\max_(i <- e `\ i) i = j -> k < \max_(i <- e) i
rewrite !inE => /andP[jDi jIe] jM.1e688ef695150a969d6a26a74826b06b6jDi:j != i
jIe:j \in e
jM:\max_(i <- e `\ i) i = j
6b1
move: H; rewrite eIE => H.1e688ef695150a969d6a24826b06b66bc6bd6beH:k.+1.-1 <= \max_(i <- e `\ i) i
6b1
apply: leq_ltn_trans H _; rewrite iM jM.1e688ef695150a969d6a24826b06b66bc6bd6be
j < i
have : j <= i by rewrite -iM; apply: leq_bigfmax.6c7j <= i -> j < i
by rewrite leq_eqVlt (negPf jDi).
Qed.

Lemma psi_aux_card_le l e : (psi_aux l `[#|`e|] <= psi_aux l e)%R.128(ψ'(l) `[#|` e|] <= ψ'(l) e)%R
Proof.6ce
rewrite ler_sub // ler_nat leq_add2l.128\sum_(i <- `[#|` e|]) 2 ^ minn (∇i) l <=
\sum_(i <- e) 2 ^ minn (∇i) l
rewrite (sum_sint (fun i =>  2 ^ minn (∇i) l)) //.128\sum_(i < #|` e|) 2 ^ minn (∇i) l <=
\sum_(i <- e) 2 ^ minn (∇i) l
have [n cI] := ubnP #|`e|; elim: n => // [] [|n] IH e cI in e cI *.f6IH:forall e,
#|` e| < 0 ->
\sum_(i < #|` e|) 2 ^ minn (∇i) l <=
\sum_(i <- e) 2 ^ minn (∇i) l
ef684
6d9
305IH:forall e,
#|` e| < n.+1 ->
\sum_(i < #|` e|) 2 ^ minn (∇i) l <=
\sum_(i <- e) 2 ^ minn (∇i) l
ef689
6d9
  by move: cI; rewrite ltnS leqn0 => /eqP-> ; rewrite big_ord0.6e16d9
move: cI; rewrite leq_eqVlt => /orP[/eqP [] eC|]; last first.3056e2ef
#|` e|.+1 < n.+2 ->
\sum_(i < #|` e|) 2 ^ minn (∇i) l <=
\sum_(i <- e) 2 ^ minn (∇i) l
3056e2efeC:#|` e| = n.+1
6d9
  by apply: IH.6ed6d9
have /(eq_fbigmax id)[/= i [iIe iM]] : 0 < #|`e| by rewrite -ltnS eC.3056e2ef6ee150a969d
6d9
have eE : #|` e| = #|` e `\ i|.+1 by rewrite (cardfsD1 i) iIe.3056e2ef6ee150a969d6a2
6d9
rewrite eE big_ord_recr /= (big_fsetD1 i) //= addnC.6f92 ^ minn (∇#|` e `\ i|) l +
\sum_(i0 < #|` e `\ i|) 2 ^ minn (∇i0) l <=
2 ^ minn (∇i) l + \sum_(i <- e `\ i) 2 ^ minn (∇i) l
apply: leq_add; last by apply: IH; rewrite -eC eE.6f92 ^ minn (∇#|` e `\ i|) l <= 2 ^ minn (∇i) l
rewrite leq_exp2l // leq_min geq_minr andbT.6f9minn (∇#|` e `\ i|) l <= ∇i
apply: leq_trans (geq_minl _ _) _.6f9∇#|` e `\ i| <= ∇i
apply: troot_le.6f9#|` e `\ i| <= i
rewrite -{2}iM -ltnS -eE -[#|`_|]prednK; last by rewrite eC.6f9#|` e|.-1 < (\max_(i <- e) i).+1
by apply: max_set_nat.
Qed.

(* This is 2.4.2 *)
Lemma psi_card_le e : psi `[#|`e|] <= psi e.eeψ(`[#|` e|]) <= ψ(e)
Proof.713
apply: psi_aux_le_psi => l.1af6d0
by apply: psi_aux_card_le.
Qed.

(* This is 2.4.3 *)
Lemma psi_exp e : psi e <= (2 ^ #|`e|).-1.eeψ(e) <= (2 ^ #|` e|).-1
Proof.71b
rewrite -(ler_nat int_numDomainType).ee(ψ(e)%:R <= (2 ^ #|` e|).-1%:R)%R
have [l ->] := psiE e.1af(ψ'(l) e <= (2 ^ #|` e|).-1%:R)%R
apply: le_trans (_ : ((2 ^ l).-1 + \sum_(i <- e) 2 ^ l)%:R - 
                      (l * 2 ^ l)%:R <= _)%R.1af(ψ'(l) e <=
 ((2 ^ l).-1 + \sum_(i <- e) 2 ^ l)%:R -
 (l * 2 ^ l)%:R)%R
1af(((2 ^ l).-1 + \sum_(i <- e) 2 ^ l)%:R -
 (l * 2 ^ l)%:R <= (2 ^ #|` e|).-1%:R)%R
  apply: ler_sub => //.1af(((2 ^ l).-1 + \sum_(i <- e) 2 ^ minn (∇i) l)%:R <=
 ((2 ^ l).-1 + \sum_(i <- e) 2 ^ l)%:R)%R
72b
  rewrite ler_nat leq_add2l.1af\sum_(i <- e) 2 ^ minn (∇i) l <= \sum_(i <- e) 2 ^ l
72b
  apply: leq_sum => i Hi.eff611fHi:true
2 ^ minn (∇i) l <= 2 ^ l
72b
  by rewrite leq_exp2l // geq_minr.1af72d
rewrite fsum_nat_const ler_subl_addr -natrD ler_nat [X in _ <= X]addnC.1af(2 ^ l).-1 + #|` e| * 2 ^ l <=
l * 2 ^ l + (2 ^ #|` e|).-1
rewrite -prednDl ?expn_gt0 // -prednDr ?expn_gt0 //.1af(2 ^ l + #|` e| * 2 ^ l).-1 <=
(l * 2 ^ l + 2 ^ #|` e|).-1
rewrite -!subn1 leq_sub2r //.1af2 ^ l + #|` e| * 2 ^ l <= l * 2 ^ l + 2 ^ #|` e|
have [E|E] := leqP #|`e| l.eff6E:#|` e| <= l
74a
eff6E:l < #|` e|
74a
  rewrite -(subnK E).74e2 ^ (l - #|` e| + #|` e|) +
#|` e| * 2 ^ (l - #|` e| + #|` e|) <=
(l - #|` e| + #|` e|) * 2 ^ (l - #|` e| + #|` e|) +
2 ^ #|` e|
750
  set u := _ - _.eff674fu:=l - #|` e|:nat
2 ^ (u + #|` e|) + #|` e| * 2 ^ (u + #|` e|) <=
(u + #|` e|) * 2 ^ (u + #|` e|) + 2 ^ #|` e|
750
  rewrite expnD !mulnDl addnAC leq_add2r.75b2 ^ u * 2 ^ #|` e| <=
u * (2 ^ u * 2 ^ #|` e|) + 2 ^ #|` e|
750
  case: u => [|u]; first by rewrite mul1n.eff674fu:nat
2 ^ u.+1 * 2 ^ #|` e| <=
u.+1 * (2 ^ u.+1 * 2 ^ #|` e|) + 2 ^ #|` e|
750
  by rewrite mulSn -addnA leq_addr.75274a
rewrite -(subnK (ltnW E)).7522 ^ l + (#|` e| - l + l) * 2 ^ l <=
l * 2 ^ l + 2 ^ (#|` e| - l + l)
set u := _ - _.eff6753u:=#|` e| - l:nat
2 ^ l + (u + l) * 2 ^ l <= l * 2 ^ l + 2 ^ (u + l)
rewrite expnD !mulnDl addnA addnC leq_add2l.7722 ^ l + u * 2 ^ l <= 2 ^ u * 2 ^ l
by rewrite -mulSn leq_mul2r ltn_expl // orbT.
Qed.

(* This is 2.5 *)
Lemma psi_diff e1 e2 : psi e1 - psi e2 <= \sum_(i <- e1 `\` e2) 2 ^ troot i.28fψ(e1) - ψ(e2) <= \sum_(i <- e1 `\` e2) 2 ^ ∇i
Proof.77a
rewrite leq_subLR -(ler_nat int_numDomainType) natrD addrC -ler_subl_addr.28f(ψ(e1)%:R - ψ(e2)%:R <=
 (\sum_(i <- e1 `\` e2) 2 ^ ∇i)%:R)%R
have [l ->] := psiE e1.f7f6
(ψ'(l) e1 - ψ(e2)%:R <=
 (\sum_(i <- e1 `\` e2) 2 ^ ∇i)%:R)%R
apply: le_trans (ler_sub (lexx _) (psi_max _ l)) _.785(ψ'(l) e1 - ψ'(l) e2 <=
 (\sum_(i <- e1 `\` e2) 2 ^ ∇i)%:R)%R
rewrite /psi_aux opprB addrA subrK addnC !natrD opprD addrA addrK.785((\sum_(i <- e1) 2 ^ minn (∇i) l)%:R -
 (\sum_(i <- e2) 2 ^ minn (∇i) l)%:R <=
 (\sum_(i <- e1 `\` e2) 2 ^ ∇i)%:R)%R
rewrite ler_subl_addr -natrD ler_nat addnC -leq_subLR.785\sum_(i <- e1) 2 ^ minn (∇i) l -
\sum_(i <- e2) 2 ^ minn (∇i) l <=
\sum_(i <- e1 `\` e2) 2 ^ ∇i
set s1 := \sum_(_ <- _) _; set s2 := \sum_(_ <- _) _; set s3 := \sum_(_ <- _) _.f7f6s1:=\sum_(H <- e1) 2 ^ minn (∇H) l:nat
s2:=\sum_(H <- e2) 2 ^ minn (∇H) l:nat
s3:=\sum_(H <- e1 `\` e2) 2 ^ ∇H:nat
s1 - s2 <= s3
pose f i := 2 ^ minn (troot i) l.f7f6797798799f:=fun i : nat => 2 ^ minn (∇i) l:nat -> nat
79a
apply: leq_trans (_ :  \sum_(i <- e1 `\` e2) f i <= _); last first.79e\sum_(i <- e1 `\` e2) f i <= s3
79es1 - s2 <= \sum_(i <- e1 `\` e2) f i
  by apply: leq_sum => i _; rewrite leq_exp2l // geq_minl.79e7a6
rewrite leq_subLR.79es1 <= s2 + \sum_(i <- e1 `\` e2) f i
rewrite [s1](big_fsetID _ (fun i => i \in e2)) //=.79e\sum_(i <- [fset x | x in e1 & x \in e2])
   2 ^ minn (∇i) l +
\sum_(i <- [fset x | x in e1 & x \notin e2])
   2 ^ minn (∇i) l <= s2 + \sum_(i <- e1 `\` e2) f i
apply: leq_add.79e\sum_(i <- [fset x | x in e1 & x \in e2])
   2 ^ minn (∇i) l <= s2
79e\sum_(i <- [fset x | x in e1 & x \notin e2])
   2 ^ minn (∇i) l <= \sum_(i <- e1 `\` e2) f i
  rewrite [s2](big_fsetID _ (fun i => i \in e1)) //=.79e\sum_(i <- [fset x | x in e1 & x \in e2])
   2 ^ minn (∇i) l <=
\sum_(i <- [fset x | x in e2 & x \in e1])
   2 ^ minn (∇i) l +
\sum_(i <- [fset x | x in e2 & x \notin e1])
   2 ^ minn (∇i) l
7b6
  apply: leq_trans (leq_addr _ _).79e\sum_(i <- [fset x | x in e1 & x \in e2])
   2 ^ minn (∇i) l <=
\sum_(i <- [fset x | x in e2 & x \in e1])
   2 ^ minn (∇i) l
7b6
  rewrite leq_eqVlt; apply/orP; left; apply/eqP.79e\sum_(i <- [fset x | x in e1 & x \in e2])
   2 ^ minn (∇i) l =
\sum_(i <- [fset x | x in e2 & x \in e1])
   2 ^ minn (∇i) l
7b6
  by apply: eq_fbigl => i; rewrite !inE andbC.79e7b8
rewrite leq_eqVlt; apply/orP; left; apply/eqP.79e\sum_(i <- [fset x | x in e1 & x \notin e2])
   2 ^ minn (∇i) l = \sum_(i <- e1 `\` e2) f i
by apply: eq_fbigl => i; rewrite !inE andbC.
Qed.

(* This is 2.6 *)

Lemma psi_delta e s a : 
  #|` e `\` `[delta s]| <= s -> a \in e -> psi e - psi (e `\  a) <= 2 ^ s.-1.efs:nat
a:nat_choiceType
#|` e `\` `[Δs]| <= s ->
a \in e -> ψ(e) - ψ(e `\ a) <= 2 ^ s.-1
Proof.7cd
move=> CLs aIe.ef7d07d1CLs:#|` e `\` `[Δs]| <= s
aIe:a \in e
ψ(e) - ψ(e `\ a) <= 2 ^ s.-1
rewrite leq_subLR -(ler_nat int_numDomainType) natrD addrC -ler_subl_addr.7d7(ψ(e)%:R - ψ(e `\ a)%:R <= (2 ^ s.-1)%:R)%R
have [l Hl] := psiE e.ef7d07d17d87d9f6Hl:(ψ(e)%:R)%R = ψ'(l) e
7de
have F l1 : s <= l1.+1 -> (psi_aux l1.+1 e <= psi_aux l1 e)%R.ef7d07d17d87d9f67e3l1:nat
s <= l1.+1 -> (ψ'(l1.+1) e <= ψ'(l1) e)%R
ef7d07d17d87d9f67e3F:forall l1 : nat,
s <= l1.+1 -> (ψ'(l1.+1) e <= ψ'(l1) e)%R
7de 
  move=> sLl1.ef7d07d17d87d9f67e37e8sLl1:s <= l1.+1
(ψ'(l1.+1) e <= ψ'(l1) e)%R
7ea
  rewrite psi_auxE_le.7f1(((2 ^ l1.+1 * #|` [fset i | i in e & (l1 < ∇i)%N]|.+1).-1 +
  \sum_(i <- e | (∇i < l1.+1)%N) 2 ^ ∇i)%:R -
 (l1.+1 * 2 ^ l1.+1)%:R <= ψ'(l1) e)%R
7ea
  rewrite psi_auxE_lt.7f1(((2 ^ l1.+1 * #|` [fset i | i in e & (l1 < ∇i)%N]|.+1).-1 +
  \sum_(i <- e | (∇i < l1.+1)%N) 2 ^ ∇i)%:R -
 (l1.+1 * 2 ^ l1.+1)%:R <=
 ((2 ^ l1 * #|` [fset i | i in e & (l1 < ∇i)%N]|.+1).-1 +
  \sum_(i <- e | (∇i <= l1)%N) 2 ^ ∇i)%:R -
 (l1 * 2 ^ l1)%:R)%R
7ea
  set s1 := \sum_(_ <- _ | _) _.ef7d07d17d87d9f67e37e87f2s1:=\sum_(H <- e | ∇H < l1.+1) 2 ^ ∇H:nat
(((2 ^ l1.+1 * #|` [fset i | i in e & (l1 < ∇i)%N]|.+1).-1 +
  s1)%:R - (l1.+1 * 2 ^ l1.+1)%:R <=
 ((2 ^ l1 * #|` [fset i | i in e & (l1 < ∇i)%N]|.+1).-1 +
  s1)%:R - (l1 * 2 ^ l1)%:R)%R
7ea
  have -> : [fset i in e | l1 < troot i] = [fset i in e | delta l1.+1 <= i].7ff[fset i | i in e & l1 < ∇i] =
[fset i | i in e & Δl1.+1 <= i]
7ff(((2 ^ l1.+1 *
   #|` [fset i | i in e & (Δl1.+1 <= i)%N]|.+1).-1 +
  s1)%:R - (l1.+1 * 2 ^ l1.+1)%:R <=
 ((2 ^ l1 *
   #|` [fset i | i in e & (Δl1.+1 <= i)%N]|.+1).-1 +
  s1)%:R - (l1 * 2 ^ l1)%:R)%R
7eb
    by apply/fsetP => i; rewrite !inE root_delta_le.7ff808
7ea
  set c := #|`_|.ef7d07d17d87d9f67e37e87f2800c:=#|` [fset i | i in e & Δl1.+1 <= i]|:nat
(((2 ^ l1.+1 * c.+1).-1 + s1)%:R -
 (l1.+1 * 2 ^ l1.+1)%:R <=
 ((2 ^ l1 * c.+1).-1 + s1)%:R - (l1 * 2 ^ l1)%:R)%R
7ea
  have Hc : c <= s.80fc <= s
ef7d07d17d87d9f67e37e87f2800810Hc:c <= s
811
7eb
    apply: leq_trans CLs.ef7d07d17d9f67e37e87f2800810
c <= #|` e `\` `[Δs]|
816
    apply: fsubset_leq_card.81d[fset i | i in e & Δl1.+1 <= i] `<=` e `\` `[Δs]
816
    apply/fsubsetP=> i.ef7d07d17d9f67e37e87f280081011f
i \in [fset i | i in e & Δl1.+1 <= i] ->
i \in e `\` `[Δs]
816
    rewrite !inE => /andP[-> H].ef7d07d17d9f67e37e87f280081011fH:Δl1.+1 <= i
(i \notin `[Δs]) && true
816
    rewrite andbT mem_sint -leqNgt (leq_trans _ H) //.82bΔs <= Δl1.+1
816
    by apply: delta_le.818811
7ea
  rewrite expnS mulnAC [2 * _ * _]mulnC.818(((2 ^ l1 * (2 * c.+1)).-1 + s1)%:R -
 (l1.+1 * (2 * 2 ^ l1))%:R <=
 ((2 ^ l1 * c.+1).-1 + s1)%:R - (l1 * 2 ^ l1)%:R)%R
7ea
  rewrite mul2n mulnA muln2 -!addnn -[(_ + l1.+1)%N]addSnnS.818(((2 ^ l1 * (c.+1 + c.+1)).-1 + s1)%:R -
 ((l1.+2 + l1) * 2 ^ l1)%:R <=
 ((2 ^ l1 * c.+1).-1 + s1)%:R - (l1 * 2 ^ l1)%:R)%R
7ea
  rewrite mulnDl mulnDr prednDr ?(muln_gt0, expn_gt0) //.818((2 ^ l1 * c.+1 + (2 ^ l1 * c.+1).-1 + s1)%:R -
 (l1.+2 * 2 ^ l1 + l1 * 2 ^ l1)%:R <=
 ((2 ^ l1 * c.+1).-1 + s1)%:R - (l1 * 2 ^ l1)%:R)%R
7ea
  set x := 2 ^ _ * _.ef7d07d17d87d9f67e37e87f2800810819x:=2 ^ l1 * c.+1:nat
((x + x.-1 + s1)%:R -
 (l1.+2 * 2 ^ l1 + l1 * 2 ^ l1)%:R <=
 (x.-1 + s1)%:R - (l1 * 2 ^ l1)%:R)%R
7ea
  rewrite -[(_ + s1)%N]addnA [(x + _)%N]addnC.844((x.-1 + s1 + x)%:R -
 (l1.+2 * 2 ^ l1 + l1 * 2 ^ l1)%:R <=
 (x.-1 + s1)%:R - (l1 * 2 ^ l1)%:R)%R
7ea
  rewrite [X in (_ - X <= _)%R]natrD opprD addrA ler_add //.844((x.-1 + s1 + x)%:R - (l1.+2 * 2 ^ l1)%:R <=
 (x.-1 + s1)%:R)%R
7ea
  rewrite ler_sub_addr natrD ler_add // ler_nat.844x <= l1.+2 * 2 ^ l1
7ea
  by rewrite mulnC leq_mul2l ltnS (leq_trans _ sLl1) ?orbT.7ec7de
pose l1 := minn l s.-1.ef7d07d17d87d9f67e37edl1:=minn l s.-1:nat
7de
have -> : ((psi e)%:R = psi_aux l1 e)%R.859(ψ(e)%:R)%R = ψ'(l1) e
859(ψ'(l1) e - ψ(e `\ a)%:R <= (2 ^ s.-1)%:R)%R
  have [/minn_idPl U|E] := leqP l s.-1; first by rewrite [l1]U.ef7d07d17d87d9f67e37ed85aE:s.-1 < l
85e
85f
  have /ltnW/minn_idPr U := E.ef7d07d17d87d9f67e37ed85a866U:minn l s.-1 = s.-1
85e
85f
  rewrite [l1]U.86a(ψ(e)%:R)%R = ψ'(s.-1) e
85f
  apply/eqP; rewrite eq_le psi_max andbT Hl.86a(ψ'(l) e <= ψ'(s.-1) e)%R
85f
  rewrite -(subnK (ltnW E)).86a(ψ'(l - s.-1 + s.-1) e <= ψ'(s.-1) e)%R
85f
  elim: (_ - _) => [|k IH] //.ef7d07d17d87d9f67e37ed85a86686b482IH:(ψ'(k + s.-1) e <= ψ'(s.-1) e)%R
(ψ'(k.+1 + s.-1) e <= ψ'(s.-1) e)%R
85f
  apply: le_trans IH.ef7d07d17d87d9f67e37ed85a86686b482
(ψ'(k.+1 + s.-1) e <= ψ'(k + s.-1) e)%R
85f
  rewrite addSn.881(ψ'((k + s.-1).+1) e <= ψ'(k + s.-1) e)%R
85f
  apply: F => //.ef7d07d17d87d9f67e385a86686b482
s <= (k + s.-1).+1
85f
  case: (s) => // s1.ef7d07d17d87d9f67e385a86686bk, s1:nat
s1 < (k + s1.+1.-1).+1
85f
  by rewrite ltnS /= leq_addl.859861
apply: le_trans (ler_sub (lexx _) (psi_max _ l1)) _.859(ψ'(l1) e - ψ'(l1) (e `\ a) <= (2 ^ s.-1)%:R)%R
rewrite /psi_aux opprB addrA subrK addnC !natrD opprD addrA addrK.859((\sum_(i <- e) 2 ^ minn (∇i) l1)%:R -
 (\sum_(i <- e `\ a) 2 ^ minn (∇i) l1)%:R <=
 (2 ^ s.-1)%:R)%R
rewrite ler_subl_addr -natrD ler_nat addnC -leq_subLR.859\sum_(i <- e) 2 ^ minn (∇i) l1 -
\sum_(i <- e `\ a) 2 ^ minn (∇i) l1 <= 2 ^ s.-1
rewrite (big_fsetD1  a) //= addnK leq_exp2l //.859minn (∇a) l1 <= s.-1
by apply: leq_trans (geq_minr _ _) (geq_minr _ _).
Qed.

(* This is 2.7 *)
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].n, s:nat
f7
e1 `<=` `[n] ->
Δs.-1 <= n ->
#|` e2| <= s ->
ψ(e1 `|` e2) - ψ(e1) <= ψ(`[n + s]) - ψ(`[n])
Proof.8a6
move=> e1Sn.8a9f7e1Sn:e1 `<=` `[n]
Δs.-1 <= n ->
#|` e2| <= s ->
ψ(e1 `|` e2) - ψ(e1) <= ψ(`[n + s]) - ψ(`[n])
elim: s e2 => [e2 _|s IH e2 dLn Ce2].1ee1:{fset nat}
8b0e2:{fset nat}
#|` e2| <= 0 ->
ψ(e1 `|` e2) - ψ(e1) <= ψ(`[n + 0]) - ψ(`[n])
1e8b68b07d0IH:forall e2,
Δs.-1 <= n ->
#|` e2| <= s ->
ψ(e1 `|` e2) - ψ(e1) <= ψ(`[n + s]) - ψ(`[n])
8b7dLn:Δs.+1.-1 <= n
Ce2:#|` e2| <= s.+1
ψ(e1 `|` e2) - ψ(e1) <= ψ(`[n + s.+1]) - ψ(`[n])
  rewrite leqn0 cardfs_eq0 => /eqP->.8b5ψ(e1 `|` fset0) - ψ(e1) <= ψ(`[n + 0]) - ψ(`[n])
8b9
  by rewrite fsetU0 subnn.8bb8bf
have [->|[x xIe2]] := fset_0Vmem e2.8bbψ(e1 `|` fset0) - ψ(e1) <= ψ(`[n + s.+1]) - ψ(`[n])
1e8b68b07d08bc8b78bd8be327xIe2:x \in e2
8bf
  by rewrite fsetU0 subnn.8cd8bf
have dLn1 : delta (s.-1) <= n.8cdΔs.-1 <= n
1e8b68b07d08bc8b78bd8be3278cedLn1:Δs.-1 <= n
8bf
  apply: leq_trans dLn.1e8b68b07d08bc8b78be3278ce
Δs.-1 <= Δs.+1.-1
8d6
  by apply: delta_le; case: (s) => // s1 /=.8d88bf
pose e3 := e2 `\ x.1e8b68b07d08bc8b78bd8be3278ce8d9e3:=e2 `\ x:{fset nat_choiceType}
8bf
have Ce3 : #|` e3| <= s.8e5#|` e3| <= s
1e8b68b07d08bc8b78bd8be3278ce8d98e6Ce3:#|` e3| <= s
8bf
  by move: Ce2; rewrite (cardfsD1 x) xIe2 ltnS.8ed8bf
apply: leq_trans (leq_sub_add (psi (e1 `|` e3)) _ _) _.8edψ(e1 `|` e2) - ψ(e1 `|` e3) + (ψ(e1 `|` e3) - ψ(e1)) <=
ψ(`[n + s.+1]) - ψ(`[n])
rewrite addnS psi_sintS.8edψ(e1 `|` e2) - ψ(e1 `|` e3) + (ψ(e1 `|` e3) - ψ(e1)) <=
ψ(`[n + s]) + 2 ^ (∇(n + s).+1).-1 - ψ(`[n])
rewrite [X in _ <= X - _]addnC -addnBA; last first.8edψ(`[n]) <= ψ(`[n + s])
8edψ(e1 `|` e2) - ψ(e1 `|` e3) + (ψ(e1 `|` e3) - ψ(e1)) <=
2 ^ (∇(n + s).+1).-1 + (ψ(`[n + s]) - ψ(`[n]))
  by apply: psi_sint_leq; rewrite leq_addr.8ed900
apply: leq_add; last by apply: IH.8edψ(e1 `|` e2) - ψ(e1 `|` e3) <= 2 ^ (∇(n + s).+1).-1
have [xIe1|xNIe1] := boolP (x \in e1).1e8b68b07d08bc8b78bd8be3278ce8d98e68eexIe1:x \in e1
907
1e8b68b07d08bc8b78bd8be3278ce8d98e68eexNIe1:x \notin e1
907
  have -> : e1 `|` e2 = e1 `|` e3.90be1 `|` e2 = e1 `|` e3
90bψ(e1 `|` e3) - ψ(e1 `|` e3) <= 2 ^ (∇(n + s).+1).-1
90e
    apply/fsetP=> i; rewrite !inE.1e8b68b07d08bc8b78bd8be3278ce8d98e68ee90c11f
(i \in e1) || (i \in e2) =
(i \in e1) || (i != x) && (i \in e2)
915
    by case: eqP => // ->; rewrite xIe1.90b917
90d
  by rewrite subnn.90f907
have -> : e1 `|` e3 = (e1 `|` e2) `\ x.90fe1 `|` e3 = (e1 `|` e2) `\ x
90fψ(e1 `|` e2) - ψ((e1 `|` e2) `\ x) <=
2 ^ (∇(n + s).+1).-1
  apply/fsetP=> i; rewrite !inE.1e8b68b07d08bc8b78bd8be3278ce8d98e68ee91011f
(i \in e1) || (i != x) && (i \in e2) =
(i != x) && ((i \in e1) || (i \in e2))
927
  case: eqP => // ->.92d(x \in e1) || ~~ true && (x \in e2) =
~~ true && ((x \in e1) || (x \in e2))
927
  by rewrite (negPf xNIe1).90f929
apply: psi_delta; last first.90fx \in e1 `|` e2
90f#|` (e1 `|` e2) `\` `[Δ(∇(n + s).+1)]| <= ∇(n + s).+1
  by rewrite !inE xIe2 orbT.90f93c
rewrite -addnS.90f#|` (e1 `|` e2) `\` `[Δ(∇(n + s.+1))]| <= ∇(n + s.+1)
set t := s.+1.1e8b68b07d08bc8b78bd8be3278ce8d98e68ee910t:=s.+1:nat
#|` (e1 `|` e2) `\` `[Δ(∇(n + t))]| <= ∇(n + t)
set g := troot (n + t).1e8b68b07d08bc8b78bd8be3278ce8d98e68ee910948g:=∇(n + t):nat
#|` (e1 `|` e2) `\` `[Δg]| <= g
apply: leq_trans (_ : #|` e2 `|` (e1 `\` `[delta g])| <= _).94d#|` (e1 `|` e2) `\` `[Δg]| <= #|` e2 `|` e1 `\` `[Δg]|
94d#|` e2 `|` e1 `\` `[Δg]| <= g
  apply: fsubset_leq_card.94d(e1 `|` e2) `\` `[Δg] `<=` e2 `|` e1 `\` `[Δg]
954
  apply/fsubsetP=> i.1e8b68b07d08bc8b78bd8be3278ce8d98e68ee91094894e11f
i \in (e1 `|` e2) `\` `[Δg] ->
i \in e2 `|` e1 `\` `[Δg]
954
  rewrite !inE.95e(i \notin `[Δg]) && ((i \in e1) || (i \in e2)) ->
(i \in e2) || (i \notin `[Δg]) && (i \in e1)
954
  by do 2 case: (_ \in _); rewrite ?(orbT, orbF).94d956
apply: leq_trans (_ : #|` e2| + #|` e1 `\` `[delta g]| <= _).94d#|` e2 `|` e1 `\` `[Δg]| <=
#|` e2| + #|` e1 `\` `[Δg]|
94d#|` e2| + #|` e1 `\` `[Δg]| <= g
  by rewrite -cardfsUI leq_addr.94d96d
apply: leq_trans (_ : t + #|` e1 `\` `[delta g]| <= _).94d#|` e2| + #|` e1 `\` `[Δg]| <= t + #|` e1 `\` `[Δg]|
94dt + #|` e1 `\` `[Δg]| <= g
  by rewrite leq_add2r.94d977
apply: leq_trans (_ : t + #|` sint (delta g) n| <= _).94dt + #|` e1 `\` `[Δg]| <= t + #|` sint (Δg) n|
94dt + #|` sint (Δg) n| <= g
  rewrite leq_add2l.94d#|` e1 `\` `[Δg]| <= #|` sint (Δg) n|
97f
  apply: fsubset_leq_card.94de1 `\` `[Δg] `<=` sint (Δg) n
97f
  apply/fsubsetP=> i.95ei \in e1 `\` `[Δg] -> i \in sint (Δg) n
97f
  rewrite !(inE, mem_sint) /= -leqNgt => /andP[-> /(fsubsetP e1Sn)].95ei \in `[n] -> true && (i < n)
97f
  by rewrite mem_sint.94d981
rewrite card_sint.94dt + (n - Δg) <= g 
have [|E] := leqP n (delta g); last first.1e8b68b07d08bc8b78bd8be3278ce8d98e68ee91094894eE:Δg < n
998
94dn <= Δg -> t + (n - Δg) <= g
  rewrite addnBA; last by apply: ltnW.99ct + n - Δg <= g
99e
  rewrite leq_subLR addnC.99cn + t <= Δg + g
99e
  by rewrite -ltnS -!addnS -deltaS addnS -root_delta_lt.94d9a0
move/eqP->; rewrite addn0.94dt <= g
by rewrite root_delta_le deltaS leq_add2r.
Qed.

(* This is 2.8 *)
Lemma psi_cap_ge e1 e2 : phi (#|` e1 `|` e2|.+3) <= (psi e1 + psi e2).*2.*2 + 5.28fϕ(#|` e1 `|` e2|.+3) <= ((ψ(e1) + ψ(e2)).*2).*2 + 5
Proof.9b1
rewrite -(ler_nat int_numDomainType) natrD.28f(ϕ(#|` e1 `|` e2|.+3)%:R <=
 ((ψ(e1) + ψ(e2)).*2).*2%:R + 5%:R)%R
rewrite -!muln2 !natrM !mulr_natr -mulrnA natrD.28f(ϕ(#|` e1 `|` e2|.+3)%:R <=
 (ψ(e1)%:R + ψ(e2)%:R) *+ (2 * 2) + 5%:R)%R
set n := #|`_|.f7n:=#|` e1 `|` e2|:nat
(ϕ(n.+3)%:R <= (ψ(e1)%:R + ψ(e2)%:R) *+ (2 * 2) + 5%:R)%R
pose m := troot (n.+3).f79c1m:=∇n.+3:nat
9c2
pose p := tmod (n.+3).f79c19c7p:=tmod n.+3:nat
9c2
pose l := m.-2.f79c19c79ccl:=m.-2:nat
9c2
have mG2 : m >= 2 by rewrite root_delta_le.f79c19c79cc9d1mG2:1 < m
9c2
have pLm : p <= m.9d5p <= m
f79c19c79cc9d19d6pLm:p <= m
9c2
  by rewrite leq_subLR -ltnS -[X in _ < X]addnS -deltaS -root_delta_lt ltnS.9dd9c2
have nG : n >= delta l.9ddΔl <= n
f79c19c79cc9d19d69denG:Δl <= n
9c2
  rewrite -[n]/(n.+3.-2.-1) [n.+3]tmodE /l -/m.9ddΔm.-2 <= (Δm + tmod n.+3).-1.-2
9e6
  case: (m) mG2 => // [] [|] // m1 _.f79c19c79cc9d19dem1:nat
Δm1.+2.-2 <= (Δm1.+2 + tmod n.+3).-1.-2
9e6
  by rewrite deltaS deltaS /= !(addSn, addnS, subSS, subn0) -!addnA leq_addr.9e89c2
apply: le_trans (_ : ((psi_aux l `[0] + psi_aux l `[n]) *+ 4 + 5%:R <= _))%R; 
     last first.9e8((ψ'(l) `[0] + ψ'(l) `[n]) *+ 4 + 5%:R <=
 (ψ(e1)%:R + ψ(e2)%:R) *+ (2 * 2) + 5%:R)%R
9e8(ϕ(n.+3)%:R <= (ψ'(l) `[0] + ψ'(l) `[n]) *+ 4 + 5%:R)%R
  rewrite ler_add2r ler_muln2r orFb.9e8(ψ'(l) `[0] + ψ'(l) `[n] <= ψ(e1)%:R + ψ(e2)%:R)%R
9fb
  apply: le_trans (_ : psi_aux l e1 + psi_aux l e2 <= _)%R; last first.9e8(ψ'(l) e1 + ψ'(l) e2 <= ψ(e1)%:R + ψ(e2)%:R)%R
9e8(ψ'(l) `[0] + ψ'(l) `[n] <= ψ'(l) e1 + ψ'(l) e2)%R
9fc
    by apply: ler_add; apply: psi_max.9e8a08
9fb
  apply: le_trans (_ : psi_aux l (e1 `&` e2) + psi_aux l (e1 `|` e2) <= _)%R.9e8(ψ'(l) `[0] + ψ'(l) `[n] <=
 ψ'(l) (e1 `&` e2) + ψ'(l) (e1 `|` e2))%R
9e8(ψ'(l) (e1 `&` e2) + ψ'(l) (e1 `|` e2) <=
 ψ'(l) e1 + ψ'(l) e2)%R
9fc
    apply: ler_add; last by apply: psi_aux_card_le.9e8(ψ'(l) `[0] <= ψ'(l) (e1 `&` e2))%R
a10
    apply: psi_aux_sub; rewrite sint0_set0.9e8fset0 `<=` e1 `&` e2
a10
    by apply/fsubsetP=> i; rewrite inE.9e8a12
9fb
  rewrite /psi_aux.9e8(((2 ^ l).-1 + \sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R +
 (((2 ^ l).-1 +
   \sum_(i <- (e1 `|` e2)) 2 ^ minn (∇i) l)%:R -
  (l * 2 ^ l)%:R) <=
 ((2 ^ l).-1 + \sum_(i <- e1) 2 ^ minn (∇i) l)%:R -
 (l * 2 ^ l)%:R +
 (((2 ^ l).-1 + \sum_(i <- e2) 2 ^ minn (∇i) l)%:R -
  (l * 2 ^ l)%:R))%R
9fb
  rewrite !natrD !addrA ler_add // -!addrA ler_add //.9e8((\sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l)%:R +
 (1 *- (l * 2 ^ l) +
  ((2 ^ l).-1%:R +
   (\sum_(i <- (e1 `|` e2)) 2 ^ minn (∇i) l)%:R)) <=
 (\sum_(i <- e1) 2 ^ minn (∇i) l)%:R +
 (1 *- (l * 2 ^ l) +
  ((2 ^ l).-1%:R + (\sum_(i <- e2) 2 ^ minn (∇i) l)%:R)))%R
9fb
  rewrite addrCA [X in (_ <= X)%R]addrCA ler_add //.9e8((\sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l)%:R +
 ((2 ^ l).-1%:R +
  (\sum_(i <- (e1 `|` e2)) 2 ^ minn (∇i) l)%:R) <=
 (\sum_(i <- e1) 2 ^ minn (∇i) l)%:R +
 ((2 ^ l).-1%:R + (\sum_(i <- e2) 2 ^ minn (∇i) l)%:R))%R
9fb
  rewrite addrCA [X in (_ <= X)%R]addrCA ler_add //.9e8((\sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l)%:R +
 (\sum_(i <- (e1 `|` e2)) 2 ^ minn (∇i) l)%:R <=
 (\sum_(i <- e1) 2 ^ minn (∇i) l)%:R +
 (\sum_(i <- e2) 2 ^ minn (∇i) l)%:R)%R
9fb
  rewrite -!natrD ler_nat.9e8\sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l +
\sum_(i <- (e1 `|` e2)) 2 ^ minn (∇i) l <=
\sum_(i <- e1) 2 ^ minn (∇i) l +
\sum_(i <- e2) 2 ^ minn (∇i) l
9fb
  rewrite [X in _ <= X + _](bigID (fun i => i \in e2)) /=.9e8\sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l +
\sum_(i <- (e1 `|` e2)) 2 ^ minn (∇i) l <=
\sum_(i <- e1 | i \in e2) 2 ^ minn (∇i) l +
\sum_(i <- e1 | i \notin e2) 2 ^ minn (∇i) l +
\sum_(i <- e2) 2 ^ minn (∇i) l
9fb
  rewrite -!addnA leq_add //.9e8\sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l <=
\sum_(i <- e1 | i \in e2) 2 ^ minn (∇i) l
9e8\sum_(i <- (e1 `|` e2)) 2 ^ minn (∇i) l <=
\sum_(i <- e1 | i \notin e2) 2 ^ minn (∇i) l +
\sum_(i <- e2) 2 ^ minn (∇i) l
9fc
    rewrite leq_eqVlt; apply/orP; left; apply/eqP.9e8\sum_(i <- e1 `&` e2) 2 ^ minn (∇i) l =
\sum_(i <- e1 | i \in e2) 2 ^ minn (∇i) l
a3a
    by apply: eq_fbigl_cond => i; rewrite !inE /= andbT.9e8a3c
9fb
  rewrite [X in X <= _](bigID (fun i => i \in e2)) /=.9e8\sum_(i <- (e1 `|` e2) | i \in e2) 2 ^ minn (∇i) l +
\sum_(i <- (e1 `|` e2) | i \notin e2) 2 ^ minn (∇i) l <=
\sum_(i <- e1 | i \notin e2) 2 ^ minn (∇i) l +
\sum_(i <- e2) 2 ^ minn (∇i) l
9fb
  rewrite addnC leq_add //.9e8\sum_(i <- (e1 `|` e2) | i \notin e2) 2 ^ minn (∇i) l <=
\sum_(i <- e1 | i \notin e2) 2 ^ minn (∇i) l
9e8\sum_(i <- (e1 `|` e2) | i \in e2) 2 ^ minn (∇i) l <=
\sum_(i <- e2) 2 ^ minn (∇i) l
9fc
    rewrite leq_eqVlt; apply/orP; left; apply/eqP.9e8\sum_(i <- (e1 `|` e2) | i \notin e2) 2 ^ minn (∇i) l =
\sum_(i <- e1 | i \notin e2) 2 ^ minn (∇i) l
a4c
    apply: eq_fbigl_cond => i; rewrite !inE /=.f79c19c79cc9d19d69de9e911f
((i \in e1) || (i \in e2)) && (i \notin e2) =
(i \in [eta mem_seq e1]) && (i \notin e2)
a4c
    by case: (_ \in e2); rewrite ?(andbT, orbT, andbF, orbF).9e8a4e
9fb
  rewrite leq_eqVlt; apply/orP; left; apply/eqP.9e8\sum_(i <- (e1 `|` e2) | i \in e2) 2 ^ minn (∇i) l =
\sum_(i <- e2) 2 ^ minn (∇i) l
9fb
  apply: eq_fbigl_cond => i; rewrite !inE /=.a56((i \in e1) || (i \in e2)) && (i \in e2) =
(i \in [eta mem_seq e2]) && true
9fb
  by case: (_ \in e2); rewrite /= ?(andbT, orbT, andbF, orbF).9e89fd
have pE : phi (n.+3) = ((m + p - 1) * 2 ^ m).+1.9e8ϕ(n.+3) = ((m + p - 1) * 2 ^ m).+1
f79c19c79cc9d19d69de9e9pE:ϕ(n.+3) = ((m + p - 1) * 2 ^ m).+1
9fd
  rewrite phi_modE -/m -/p -{1 4}[m]prednK 1?ltnW //.9e81 + (m.-1.+1 + p) * 2 ^ m - 2 ^ m =
((m.-1.+1 + p - 1) * 2 ^ m).+1
a6a
  rewrite [(_ + p)%N]addSn mulSn [(2 ^ _ + _)%nat]addnC addnA addnK.9e8(1 + (m.-1 + p) * 2 ^ m)%N =
(((m.-1 + p).+1 - 1) * 2 ^ m).+1
a6a
  by rewrite -subn1 -[(_ + _).+1]addn1 addnK.a6c9fd
have pdE : ((phi (delta l))%:R = 1 + (l%:R - 1) * (2 ^ l)%:R :> int)%R.a6c(ϕ(Δl)%:R)%R = (1 + (l%:R - 1) * (2 ^ l)%:R)%R
f79c19c79cc9d19d69de9e9a6dpdE:(ϕ(Δl)%:R)%R = (1 + (l%:R - 1) * (2 ^ l)%:R)%R
9fd
  rewrite phi_deltaE natrB; last first.a6c2 ^ l <= 1 + l * 2 ^ l
a6c((1 + l * 2 ^ l)%:R - (2 ^ l)%:R)%R =
(1 + (l%:R - 1) * (2 ^ l)%:R)%R
a7e
    by case: (l) => // l1; rewrite mulSn addnCA leq_addr.a6ca87
a7d
  by rewrite natrD /= mulrBl mul1r addrA -natrM.a7f9fd
rewrite le_eqVlt; apply/orP; left; apply/eqP.a7f(ϕ(n.+3)%:R)%R =
((ψ'(l) `[0] + ψ'(l) `[n]) *+ 4 + 5%:R)%R
(* right part *)
rewrite psi_aux_sintE // psi_auxE_le.a7f(ϕ(n.+3)%:R)%R =
((((2 ^ l).-1 + \sum_(0 <= i < 0) 2 ^ minn (∇i) l)%:R -
  (l * 2 ^ l)%:R +
  (((2 ^ l *
     #|` [fset i | i in `[n] & (l <= ∇i)%N]|.+1).-1 +
    \sum_(i <- `[n] | (∇i < l)%N) 2 ^ ∇i)%:R -
   (l * 2 ^ l)%:R)) *+ 4 + 5%:R)%R
pose f i := 2 ^ minn (∇i) l.f79c19c79cc9d19d69de9e9a6da8079f
a95
rewrite !(big_mkord _ f) big_ord0 addn0.a99(ϕ(n.+3)%:R)%R =
(((2 ^ l).-1%:R - (l * 2 ^ l)%:R +
  (((2 ^ l *
     #|` [fset i | i in `[n] & (l <= ∇i)%N]|.+1).-1 +
    \sum_(i <- `[n] | (∇i < l)%N) 2 ^ ∇i)%:R -
   (l * 2 ^ l)%:R)) *+ 4 + 5%:R)%R
have -> : [fset i in `[n] | l <= troot i] = [fset i in `[n] | delta l <= i].a99[fset i | i in `[n] & l <= ∇i] =
[fset i | i in `[n] & Δl <= i]
a99(ϕ(n.+3)%:R)%R =
(((2 ^ l).-1%:R - (l * 2 ^ l)%:R +
  (((2 ^ l *
     #|` [fset i | i in `[n] & (Δl <= i)%N]|.+1).-1 +
    \sum_(i <- `[n] | (∇i < l)%N) 2 ^ ∇i)%:R -
   (l * 2 ^ l)%:R)) *+ 4 + 5%:R)%R
  by apply/fsetP=> i; rewrite !inE root_delta_le.a99aa4
have /(sint_sub n)-> : 0 <= delta l.a990 <= Δl
a99(ϕ(n.+3)%:R)%R =
(((2 ^ l).-1%:R - (l * 2 ^ l)%:R +
  (((2 ^ l * #|` sint (Δl) n|.+1).-1 +
    \sum_(i <- `[n] | (∇i < l)%N) 2 ^ ∇i)%:R -
   (l * 2 ^ l)%:R)) *+ 4 + 5%:R)%R
  by apply: (@delta_le 0).a99aae
rewrite card_sint //.a99(ϕ(n.+3)%:R)%R =
(((2 ^ l).-1%:R - (l * 2 ^ l)%:R +
  (((2 ^ l * (n - Δl).+1).-1 +
    \sum_(i <- `[n] | (∇i < l)%N) 2 ^ ∇i)%:R -
   (l * 2 ^ l)%:R)) *+ 4 + 5%:R)%R
rewrite (_ : \sum_(_ <- _ | _) _  = phi (delta l)); last first.a99\sum_(H <- `[n] | ∇H < l) 2 ^ ∇H = ϕ(Δl)
a99(ϕ(n.+3)%:R)%R =
(((2 ^ l).-1%:R - (l * 2 ^ l)%:R +
  (((2 ^ l * (n - Δl).+1).-1 + ϕ(Δl))%:R -
   (l * 2 ^ l)%:R)) *+ 4 + 5%:R)%R
  rewrite phiE.a99\sum_(H <- `[n] | ∇H < l) 2 ^ ∇H =
\sum_(i < Δl) 2 ^ ∇i
aba
  rewrite [LHS](eq_bigl (fun i => (i < n) && (∇i < l))); last first.a99(fun i : nat => ∇i < l) =1
(fun i : nat => (i < n) && (∇i < l))
a99\sum_(i <- `[n] | (i < n) && (∇i < l)) 2 ^ ∇i =
\sum_(i < Δl) 2 ^ ∇i
abb
    move=> i; case: leqP; rewrite ?(andbT, andbF) // root_delta_lt.f79c19c79cc9d19d69de9e9a6da8079f150
i < Δl -> true = (i < n)
ac5
    by move/(leq_trans)->.a99ac7
aba
  rewrite [RHS](eq_bigl 
        (fun i : 'I_ _ => ((i : nat) \in (enum_fset `[n])))); last first.a99xpredT =1 (fun i : 'I_(Δl) => i \in `[n])
a99\sum_(i <- `[n] | (i < n) && (∇i < l)) 2 ^ ∇i =
\sum_(i < Δl | i \in `[n]) 2 ^ ∇i
abb
    by move=> i; rewrite mem_sint (leq_trans (ltn_ord _)).a99ad6
aba
  elim: enum_fset (fset_uniq `[n]) => /= [_|a l1 IH /andP[aNIl lU]].a99\sum_(i <- [::] | (i < n) && (∇i < l)) 2 ^ ∇i =
\sum_(i < Δl | i \in [::]) 2 ^ ∇i
f79c19c79cc9d19d69de9e9a6da8079fal1:seq nat
IH:uniq l1 ->
\sum_(i <- l1 | (i < n) && (∇i < l)) 2 ^ ∇i =
\sum_(i < Δl | i \in l1) 2 ^ ∇i
aNIl:a \notin l1
lU:uniq l1
\sum_(i <- (a :: l1) | (i < n) && (∇i < l)) 2 ^ ∇i =
\sum_(i < Δl | i \in a :: l1) 2 ^ ∇i
abb
    by rewrite big_nil big1.ae0ae5
aba
  rewrite big_cons /= IH //; case: (boolP (a < n)) => aLn /=; last first.f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae465f
\sum_(i < Δl | i \in l1) 2 ^ ∇i =
\sum_(i < Δl | i \in a :: l1) 2 ^ ∇i
f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae4664
(if ∇a < l
 then (2 ^ ∇a + \sum_(i < Δl | i \in l1) 2 ^ ∇i)%N
 else \sum_(i < Δl | i \in l1) 2 ^ ∇i) =
\sum_(i < Δl | i \in a :: l1) 2 ^ ∇i
abb
    apply: eq_bigl => i; move: (ltn_ord i); rewrite inE; case: eqP => [->| //].f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae465fi:'I_(Δl)
a < Δl -> (a \in l1) = true || (a \in l1)
aee
    by move=> /leq_trans/(_ nG); rewrite (negPf aLn).af0af1
aba
  case: leqP => aLl.f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae4664aLl:l <= ∇a
aed
f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae4664aLl:∇a < l
(2 ^ ∇a + \sum_(i < Δl | i \in l1) 2 ^ ∇i)%N =
\sum_(i < Δl | i \in a :: l1) 2 ^ ∇i
abb
    apply: eq_bigl => i; move: (ltn_ord i); rewrite inE; case: eqP => [->| //].f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae4664affaf6
af7
b00
    by rewrite -root_delta_lt ltnNge aLl.b02b04
aba
  rewrite root_delta_lt in aLl.f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae4664aLl:a < Δl
b04
aba
  rewrite [RHS](bigD1 (Ordinal aLl)); apply/eqP; last by rewrite inE eqxx.b0f(2 ^ ∇a + \sum_(i < Δl | i \in l1) 2 ^ ∇i)%N ==
addn_comoid (2 ^ ∇(Ordinal aLl))
  (\big[addn_comoid/0]_(i | (i \in a :: l1) &&
                            (i != Ordinal aLl)) 2 ^ ∇i)
aba
  rewrite /= eqn_add2l; apply/eqP.b0f\sum_(i < Δl | i \in l1) 2 ^ ∇i =
\sum_(i < Δl | (i \in a :: l1) && (i != Ordinal aLl))
   2 ^ ∇i
aba
  apply: eq_bigl => i; rewrite !inE /= -val_eqE /=.f79c19c79cc9d19d69de9e9a6da8079faae1ae2ae3ae4664b10af6
(i \in l1) = ((i == a) || (i \in l1)) && (i != a)
aba
  by case: eqP (ltn_ord i) => [->|]; rewrite?(andbT, negPf aNIl).a99abc
(* right part *)
apply: etrans
 (_ : ((2 ^ l)%:R * (m.-1 + p)%:R - 1%:R) *+4 + 5%:R = _)%R; last first.a99(((2 ^ l)%:R * (m.-1 + p)%:R - 1%:R) *+ 4 + 5%:R)%R =
(((2 ^ l).-1%:R - (l * 2 ^ l)%:R +
  (((2 ^ l * (n - Δl).+1).-1 + ϕ(Δl))%:R -
   (l * 2 ^ l)%:R)) *+ 4 + 5%:R)%R
a99(ϕ(n.+3)%:R)%R =
(((2 ^ l)%:R * (m.-1 + p)%:R - 1%:R) *+ 4 + 5%:R)%R
 congr (_ *+ _ + _)%R.a99((2 ^ l)%:R * (m.-1 + p)%:R - 1%:R)%R =
((2 ^ l).-1%:R - (l * 2 ^ l)%:R +
 (((2 ^ l * (n - Δl).+1).-1 + ϕ(Δl))%:R -
  (l * 2 ^ l)%:R))%R
b25
rewrite -!subn1 ![in RHS](natrD, natrM, natrB) ?muln_gt0 ?expn_gt0 //.a99((2 ^ l)%:R * (m - 1 + p)%:R - 1%:R)%R =
((2 ^ l)%:R - 1%:R - l%:R * (2 ^ l)%:R +
 ((2 ^ l)%:R * (n - Δl).+1%:R - 1%:R + ϕ(Δl)%:R -
  l%:R * (2 ^ l)%:R))%R
b25
rewrite pdE !addrA addrK; set u := (2 ^ l)%:R%R.f79c19c79cc9d19d69de9e9a6da8079fu:=((2 ^ l)%:R)%R:Num.NumDomain.porder_ringType int_numDomainType
(u * (m - 1 + p)%:R - 1%:R)%R =
(u - 1%:R - l%:R * u + u * (n - Δl).+1%:R +
 (l%:R - 1) * u - l%:R * u)%R
b25
rewrite [(u - 1)%R]addrC -![in RHS]addrA [RHS]addrC; congr (_ - _)%R.b33(u * (m - 1 + p)%:R)%R =
(u +
 (- (l%:R * u) +
  (u * (n - Δl).+1%:R + ((l%:R - 1) * u - l%:R * u))))%R
b25
rewrite -{2}[u]mul1r ![(u * _)%R]mulrC -![(-(_ * u))%R]mulNr -!mulrDl.b33((m - 1 + p)%:R * u)%R =
((1 + (1 *- l + ((n - Δl).+1%:R + (l%:R - 1 - l%:R)))) *
 u)%R
b25
congr (_ * _)%R.b33((m - 1 + p)%:R)%R =
(1 + (1 *- l + ((n - Δl).+1%:R + (l%:R - 1 - l%:R))))%R
b25
rewrite {u}!addrA addrAC addrK.a99((m - 1 + p)%:R)%R = (1 - l%:R + (n - Δl).+1%:R - 1)%R
b25
rewrite -[(_ - _).+1]addn1 [in RHS]natrD !addrA addrK.a99((m - 1 + p)%:R)%R = (1 - l%:R + (n - Δl)%:R)%R
b25
rewrite -[n]/(n.+3.-2.-1) [n.+3]tmodE -/m -/p.a99((m - 1 + p)%:R)%R =
(1 - l%:R + ((Δm + p).-1.-2 - Δl)%:R)%R
b25
rewrite -[in RHS](subnK mG2) ![in RHS](addnS, addn0) !deltaS !(subnS, subn0).a99((m.-1 + p)%:R)%R =
(1 - l%:R +
 ((Δm.-2 + m.-2.+1 + m.-2.+2 + p).-1.-2 - Δl)%:R)%R
b25
rewrite ![in RHS](addnS, addSn) -!addnA [(delta _ + _)%nat]addnC addnK -/l.a99((m.-1 + p)%:R)%R = (1 - l%:R + (l + (l + p))%:R)%R
b25
by rewrite ![in RHS]natrD !addrA subrK /l -(natrD _ 1%nat) -natrD.a99b27
(* left part *)
rewrite pE /l.a99(((m + p - 1) * 2 ^ m).+1%:R)%R =
(((2 ^ m.-2)%:R * (m.-1 + p)%:R - 1%:R) *+ 4 + 5%:R)%R
case: (m) mG2 => // [] [|m1] //= _.f79c19c79cc9d19de9e9a6da8079f9f2
(((m1.+2 + p - 1) * 2 ^ m1.+2).+1%:R)%R =
(((2 ^ m1)%:R * (m1.+1 + p)%:R - 1%:R) *+ 4 + 5%:R)%R
rewrite addSn subn1 /=.b60(((m1.+1 + p) * 2 ^ m1.+2).+1%:R)%R =
(((2 ^ m1)%:R * (m1.+1 + p)%:R - 1%:R) *+ 4 + 5%:R)%R
rewrite (_ : 5%:R = 1 *+ 4 + 1)%R // addrA -mulrnDl.b60(((m1.+1 + p) * 2 ^ m1.+2).+1%:R)%R =
(((2 ^ m1)%:R * (m1.+1 + p)%:R - 1%:R + 1) *+ 4 + 1)%R
rewrite subrK -addn1 natrD; congr (_ + _)%R.b60(((m1.+1 + p) * 2 ^ m1.+2)%:R)%R =
((2 ^ m1)%:R * (m1.+1 + p)%:R *+ 4)%R
rewrite -[in RHS]mulr_natr -!natrM [in RHS]mulnAC mulnC.b60((2 ^ m1.+2 * (m1.+1 + p))%:R)%R =
((2 ^ m1 * 4 * (m1.+1 + p))%:R)%R
congr (_ * _)%:R%R.b602 ^ m1.+2 = 2 ^ m1 * 4
by rewrite mulnC !expnS !mulnA.
Qed.

Lemma phi_3_5_4_phi n : phi (n.+3) = (psi `[n.+2]).*2.+1.2dcϕ(n.+3) = ψ(`[n.+2]).*2.+1
Proof.b77 by rewrite psi_sint_phi prednK ?phi_gt0. Qed.

Lemma phi_3_5_4_sum n :
   phi (n.+3) = (\sum_(1 <= i < n.+3) 2 ^ troot i).+1.2dcϕ(n.+3) = (\sum_(1 <= i < n.+3) 2 ^ ∇i).+1
Proof.b7c
rewrite phiE.2dc\sum_(i < n.+3) 2 ^ ∇i =
(\sum_(1 <= i < n.+3) 2 ^ ∇i).+1
rewrite -(big_mkord xpredT (fun i => 2 ^ troot i)).2dc\sum_(0 <= i < n.+3) 2 ^ ∇i =
(\sum_(1 <= i < n.+3) 2 ^ ∇i).+1
rewrite (big_cat_nat _ _ _ (_ : 0 <= 1)) //=.2dc(\sum_(0 <= i < 1) 2 ^ ∇i +
 \sum_(1 <= i < n.+3) 2 ^ ∇i)%N =
(\sum_(1 <= i < n.+3) 2 ^ ∇i).+1
by rewrite big_nat_recl //= big_mkord big_ord0 addn0 add1n.
Qed.

End PsiDef.

Lemma ltn_diff_ord_max n (i : 'I_n.+2) : i != ord_max -> i < n.+1.1ei:'I_n.+2
i != ord_max -> i < n.+1
Proof.b8d
move/eqP/val_eqP.b8fval i != val ord_max -> i < n.+1
by have := ltn_ord i; rewrite ltnS leq_eqVlt => /orP[->|].
Qed.

Lemma lift_diff_ord_max n (i : 'I_n.+2) :
  i != ord_max -> lift ord_max (inord i) = i.b8fi != ord_max -> lift ord_max (inord i) = i
Proof.b98
move=> iDm.1eb90iDm:i != ord_max
lift ord_max (inord i) = i
apply/val_eqP; rewrite [val (lift _ _)]lift_max /= ?inordK //.b9fi < n.+1
by apply: ltn_diff_ord_max.
Qed.

Lemma set_ord_max_lift n (e : {set 'I_n.+2}) :
  e :\ ord_max = [set lift ord_max x | x in [set i | lift ord_max i \in e]].1ee:{set 'I_n.+2}
e :\ ord_max =
[set lift ord_max x
   | x : ordinal_finType n.+2.-1
   & lift ord_max x \in e]
Proof.ba7
apply/setP => i; rewrite !inE /=.1ebaai:ordinal_finType n.+2
(i != ord_max) && (i \in e) =
(i
   \in [set lift ord_max x
          | x : 'I_n.+1
          & lift ord_max x \in e])
apply/andP/imsetP => [[iH iIe]|[j //]].1ebaabb1iH:i != ord_max
a9
exists2 x : ordinal_finType n.+1,
  x \in [set i | lift ord_max i \in e] &
  i = lift ord_max x
1ebaabb1j:ordinal_finType n.+1
j \in [set i | lift ord_max i \in e] ->
i = lift ord_max j -> i != ord_max /\ i \in e
  exists (inord i).bb6inord i \in [set i | lift ord_max i \in e]
bb6i = lift ord_max (inord i)
bba
    by rewrite inE lift_diff_ord_max.bb6bc4
bb9
  by rewrite lift_diff_ord_max.bbbbbd
rewrite inE => kH ->; split => //.1ebaabb1bbckH:lift ord_max j \in e
lift ord_max j != ord_max
apply/eqP/val_eqP.bceval (lift ord_max j) != val ord_max
by rewrite [val (lift _ _)]lift_max /= neq_ltn ltn_ord.
Qed.