From mathcomp Require Import all_ssreflect 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]
From hanoi Require Import extra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Main. 

Variable a b : nat.
Hypothesis aL1 : 1 < a.
Hypothesis aLb : a < b.
Hypothesis aCb : coprime a b.

Let bL1 : 1 < b.
a, b:nat
aL1:1 < a
aLb:a < b
aCb:coprime a b
1 < b
Proof.
2 by apply: ltn_trans aLb. Qed.

Fixpoint alphal (n : nat) :=
 if n isn't n1.+1 then [:: 1; a; b]
 else
 let l := alphal n1 in
   merge leq
   (let c := head 1 l in
    let l1 := if b * c \in l then [::] else [:: b * c] in
    if a * c \in l then l1 else a * c :: l1)
   (behead l).

Definition alpha n := head 1 (alphal n).

Lemma behead_sorted (T: eqType) (r : rel T) (l : seq T) : 
  sorted r l -> sorted r (behead l).
5678
bL1:1 < b
T:eqType
r:rel T
l:seq T
sorted r l -> sorted r (behead l)
Proof.
c by case: l => //= a1 [|b1 l /andP[]]. Qed.

Lemma sorted_alphal n : sorted leq (alphal n).
5678f
n:nat
sorted leq (alphal n)
Proof.
16
elim: n => /= [|n IH]; first by rewrite ltnW //= ltnW.
5678f19
IH:sorted leq (alphal n)
sorted leq
  (merge leq
     (if a * head 1 (alphal n) \in alphal n
      then
       if b * head 1 (alphal n) \in alphal n
       then [::]
       else [:: b * head 1 (alphal n)]
      else
       a * head 1 (alphal n)
       :: (if b * head 1 (alphal n) \in alphal n
           then [::]
           else [:: b * head 1 (alphal n)]))
     (behead (alphal n)))
apply: merge_sorted; first by apply: leq_total.
1f
sorted leq
  (if a * head 1 (alphal n) \in alphal n
   then
    if b * head 1 (alphal n) \in alphal n
    then [::]
    else [:: b * head 1 (alphal n)]
   else
    a * head 1 (alphal n)
    :: (if b * head 1 (alphal n) \in alphal n
        then [::]
        else [:: b * head 1 (alphal n)]))
1f
sorted leq (behead (alphal n))
  by do 2 case: (_ \in _) => //=; rewrite leq_mul2r orbC ltnW.
1f
28
by apply: behead_sorted.
Qed.

Lemma gt0_alphal n i : i \in alphal n -> 0 < i.
5678f19
i:nat_eqType
i \in alphal n -> 0 < i
Proof.
2d
elim: n i => /= [i|n].
5678f
i:nat
i \in [:: 1; a; b] -> 0 < i
18
(forall i : nat, i \in alphal n -> 0 < i) ->
forall i : nat,
i
  \in merge leq
        (if a * head 1 (alphal n) \in alphal n
         then
          if b * head 1 (alphal n) \in alphal n
          then [::]
          else [:: b * head 1 (alphal n)]
         else
          a * head 1 (alphal n)
          :: (if b * head 1 (alphal n) \in alphal n
              then [::]
              else [:: b * head 1 (alphal n)]))
        (behead (alphal n)) -> 0 < i
  by rewrite !inE => /or3P[] /eqP-> //; rewrite ltnW // (ltn_trans aL1).
18
3b
case: (alphal n) => [/= _ i|/= a1 l IH i]; rewrite !inE.
5678f
n, i:nat
(i == a * 1) || (i == b * 1) -> 0 < i
5678f
n, a1:nat
l:seq nat
IH:forall i : nat, i \in a1 :: l -> 0 < i
37
i
  \in merge leq
        (if (a * a1 == a1) || (a * a1 \in l)
         then
          if (b * a1 == a1) || (b * a1 \in l)
          then [::]
          else [:: b * a1]
         else
          a * a1
          :: (if (b * a1 == a1) || (b * a1 \in l)
              then [::]
              else [:: b * a1])) l -> 0 < i
  by case/orP=> /eqP->; rewrite muln1 ltnW.
47
4b
have H1 : 0 < a1 by apply: IH; rewrite inE eqxx.
5678f48494a37
H1:0 < a1
4b
have IH1 i1 : i1 \in l -> 0 < i1.
5678f48494a3753
i1:nat_eqType
i1 \in l -> 0 < i1
5678f48494a3753
IH1:forall i1 : nat_eqType, i1 \in l -> 0 < i1
4b
  by move=> U; apply: IH; rewrite inE orbC U.
5c
4b
rewrite mem_merge.
5c
i
  \in (if (a * a1 == a1) || (a * a1 \in l)
       then
        if (b * a1 == a1) || (b * a1 \in l)
        then [::]
        else [:: b * a1]
       else
        a * a1
        :: (if (b * a1 == a1) || (b * a1 \in l)
            then [::]
            else [:: b * a1])) ++ l -> 0 < i
(do 2 case: (_ || _)); rewrite //= ?inE; first by apply: IH1.
5c
(i == b * a1) || (i \in l) -> 0 < i
5c
(i == a * a1) || (i \in l) -> 0 < i
5c
[|| i == a * a1, i == b * a1 | i \in l] -> 0 < i
-
66 by case/orP=> [/eqP->|/IH1//]; rewrite muln_gt0 ltnW.
5c
6b
6c
-
70 by case/orP=> [/eqP->|/IH1//]; rewrite muln_gt0 ltnW.
5c
6d
by case/or3P=> [/eqP->|/eqP->|/IH1//]; rewrite muln_gt0 ltnW.
Qed.

Lemma alphal_neq_nil n : alphal n != nil.
18
alphal n != [::]
Proof.
78
case: n => //= n.
18
merge leq
  (if a * head 1 (alphal n) \in alphal n
   then
    if b * head 1 (alphal n) \in alphal n
    then [::]
    else [:: b * head 1 (alphal n)]
   else
    a * head 1 (alphal n)
    :: (if b * head 1 (alphal n) \in alphal n
        then [::]
        else [:: b * head 1 (alphal n)]))
  (behead (alphal n)) != [::]
rewrite -size_eq0 size_merge.
18
size
  ((if a * head 1 (alphal n) \in alphal n
    then
     if b * head 1 (alphal n) \in alphal n
     then [::]
     else [:: b * head 1 (alphal n)]
    else
     a * head 1 (alphal n)
     :: (if b * head 1 (alphal n) \in alphal n
         then [::]
         else [:: b * head 1 (alphal n)])) ++
   behead (alphal n)) != 0
case: (alphal n) (@gt0_alphal n) => //= c l H.
5678f
n, c:nat
49
H:forall i : nat, i \in c :: l -> 0 < i
size
  ((if a * c \in c :: l
    then if b * c \in c :: l then [::] else [:: b * c]
    else
     a * c
     :: (if b * c \in c :: l then [::] else [:: b * c])) ++
   l) != 0
case E : (_ \in _) => //; case : (_ \in _) => //.
5678f884989
E:(a * c \in c :: l) = true
size ([::] ++ l) != 0
case: l H E aL1 => // /(_ c); rewrite !inE eqxx => /(_ is_true_true).
5678f88
0 < c ->
(a * c == c) = true ->
1 < a -> size ([::] ++ [::]) != 0
case: c => // c1 _.
5678f
n, c1:nat
(a * c1.+1 == c1.+1) = true ->
1 < a -> size ([::] ++ [::]) != 0
by rewrite -{2}[_.+1]mul1n eqn_mul2r /= => /idP/eqP->.
Qed.

Lemma uniq_alphal n : uniq (alphal n).
18
uniq (alphal n)
Proof.
9d
elim: n =>  /=[|n IH].
5678f
[&& 1 \notin [:: a; b], a \notin [:: b] & true]
5678f19
IH:uniq (alphal n)
uniq
  (merge leq
     (if a * head 1 (alphal n) \in alphal n
      then
       if b * head 1 (alphal n) \in alphal n
       then [::]
       else [:: b * head 1 (alphal n)]
      else
       a * head 1 (alphal n)
       :: (if b * head 1 (alphal n) \in alphal n
           then [::]
           else [:: b * head 1 (alphal n)]))
     (behead (alphal n)))
  by rewrite !inE negb_or !neq_ltn aL1 aLb /= (ltn_trans aL1).
a8
aa
case: (alphal n) (@gt0_alphal n) IH => //= [_ _|c l U /andP[cL uL]].
18
(a * 1 \notin [:: b * 1]) && true
5678f8849
U:forall i : nat, i \in c :: l -> 0 < i
cL:c \notin l
uL:uniq l
uniq
  (merge leq
     (if a * c \in c :: l
      then
       if b * c \in c :: l then [::] else [:: b * c]
      else
       a * c
       :: (if b * c \in c :: l
           then [::]
           else [:: b * c])) l)
  by rewrite !inE !muln1 neq_ltn aLb.
b4
b8
(have [H1|H1] := boolP (_ \in _); have [H2|H2] := boolP (_ \in _); 
         rewrite merge_uniq); rewrite /= ?uL ?andbT //=.
5678f8849b5b6b7
H1:a * c \in c :: l
H2:b * c \notin c :: l
b * c \notin l
5678f8849b5b6b7
H1:a * c \notin c :: l
H2:b * c \in c :: l
a * c \notin l
5678f8849b5b6b7c6c1
(a * c \notin b * c :: l) && (b * c \notin l)
-
bd by move: H2; rewrite inE negb_or => /andP[].
c5
c8
c9
-
ce by move: H1; rewrite inE negb_or => /andP[].
ca
cb
move: H1 H2; rewrite !inE !negb_or => /andP[_ ->] /andP[_ ->].
b4
(a * c != b * c) && true && true
by rewrite eqn_mul2r negb_or !neq_ltn aLb U ?orbT // inE eqxx.
Qed.

Lemma alpha_ltn n : alpha n < alpha n.+1.
18
alpha n < alpha n.+1
Proof.
da
rewrite /alpha /=.
18
head 1 (alphal n) <
head 1
  (merge leq
     (if a * head 1 (alphal n) \in alphal n
      then
       if b * head 1 (alphal n) \in alphal n
       then [::]
       else [:: b * head 1 (alphal n)]
      else
       a * head 1 (alphal n)
       :: (if b * head 1 (alphal n) \in alphal n
           then [::]
           else [:: b * head 1 (alphal n)]))
     (behead (alphal n)))
set h := head _ _.
5678f19
h:=head 1 (alphal n):nat
h <
head 1
  (merge leq
     (if a * h \in alphal n
      then
       if b * h \in alphal n then [::] else [:: b * h]
      else
       a * h
       :: (if b * h \in alphal n
           then [::]
           else [:: b * h])) (behead (alphal n)))
have hP : 0 < h.
e5
0 < h
5678f19e6
hP:0 < h
e7
  rewrite /h.
e5
0 < head 1 (alphal n)
ec
  case: (alphal n) (@gt0_alphal n) => // c l /(_ c)-> //.
5678f19e6
c:nat
49
c \in c :: l
ec
  by rewrite inE eqxx.
ee
e7
set l1 := merge _ _ _.
5678f19e6ef
l1:=merge leq
  (if a * h \in alphal n
   then
    if b * h \in alphal n
    then [::]
    else [:: b * h]
   else
    a * h
    :: (if b * h \in alphal n
        then [::]
        else [:: b * h])) (behead (alphal n)):seq nat
h < head 1 l1
have hIl1 : head 1 l1 \in l1.
100
head 1 l1 \in l1
5678f19e6ef101
hIl1:head 1 l1 \in l1
102
  have /= := alphal_neq_nil n.+1.
100
merge leq
  (if a * head 1 (alphal n) \in alphal n
   then
    if b * head 1 (alphal n) \in alphal n
    then [::]
    else [:: b * head 1 (alphal n)]
   else
    a * head 1 (alphal n)
    :: (if b * head 1 (alphal n) \in alphal n
        then [::]
        else [:: b * head 1 (alphal n)]))
  (behead (alphal n)) != [::] -> head 1 l1 \in l1
107
  by rewrite -/l1; case: l1 => //= c l; rewrite inE eqxx.
109
102
suff hLi i :  i \in l1 -> h < i.
5678f19e6ef10110a
hLi:forall i : nat_eqType, i \in l1 -> h < i
102
5678f19e6ef
l1:=merge leq
  (if a * h \in alphal n
   then
    if b * h \in alphal n
    then [::]
    else [:: b * h]
   else
    a * h
    :: (if b * h \in alphal n
        then [::]
        else [:: b * h])) 
  (behead (alphal n)):seq nat
10a30
i \in l1 -> h < i
  by apply/hLi/hIl1.
5678f19e6ef10110a30
11b
rewrite mem_merge mem_cat.
11f
(i
   \in (if a * h \in alphal n
        then
         if b * h \in alphal n
         then [::]
         else [:: b * h]
        else
         a * h
         :: (if b * h \in alphal n
             then [::]
             else [:: b * h])))
|| (i \in behead (alphal n)) -> h < i
suff hLi1 : (i \in behead (alphal n)) -> h < i => [|H].
5678f19e6ef10110a30
hLi1:i \in behead (alphal n) -> h < i
123
5678f19e6ef11a10a30
H:i \in behead (alphal n)
h < i
  have [H1|H1] := boolP (_ \in alphal _);
    have [H2|H2] := boolP (_ \in alphal _); rewrite /= ?inE -/h //.
5678f19e6ef10110a30128
H1:a * h \in alphal n
H2:b * h \notin alphal n
(i == b * h) || (i \in behead (alphal n)) -> h < i
5678f19e6ef11a10a30128
H1:a * h \notin alphal n
H2:b * h \in alphal n
(i == a * h) || (i \in behead (alphal n)) -> h < i
5678f19e6ef11a10a30128138133
(i == a * h) || (i == b * h)
|| (i \in behead (alphal n)) -> 
h < i
12a
  -
12f by case/orP=> [/eqP->|//]; rewrite ltn_Pmull.
5678f19e6ef10110a30128138139
13a
13b12a
  -
140 by case/orP=> [/eqP->|//]; rewrite ltn_Pmull.
5678f19e6ef10110a30128138133
(i == a * h) || (i == b * h)
|| (i \in behead (alphal n)) -> h < i
129
  by rewrite -orbA => /or3P[/eqP->|/eqP->|//]; rewrite ltn_Pmull.
5678f19e6ef10110a3012c
12d
have hsSa : subseq [:: h; i] (alphal n).
14d
subseq [:: h; i] (alphal n)
5678f19e6ef11a10a3012c
hsSa:subseq [:: h; i] (alphal n)
12d
  rewrite (_ : alphal n =  h :: behead (alphal n)).
14d
subseq [:: h; i] (h :: behead (alphal n))
12b
alphal n = h :: behead (alphal n)
153
    rewrite (@cat_subseq _ [::h] _ [::h]) //.
14d
subseq [:: i] (behead (alphal n))
15a
    by rewrite sub1seq.
14d
15c
152
  by rewrite /h; case: (alphal n) (alphal_neq_nil n).
5678f19e6ef10110a3012c155
12d
rewrite ltn_neqAle.
167
(h != i) && (h <= i)
have /= := subseq_sorted leq_trans hsSa (sorted_alphal n).
167
(h <= i) && true -> (h != i) && (h <= i)
rewrite andbT => ->.
167
(h != i) && true
have /= := subseq_uniq hsSa (uniq_alphal n).
167
(h \notin [:: i]) && true -> (h != i) && true
by rewrite inE.
Qed.

Lemma alpha_mono m n : m < n -> alpha m < alpha n.
5678f
m, n:nat
m < n -> alpha m < alpha n
Proof.
179
elim: n => // n IH.
5678f17c
IH:m < n -> alpha m < alpha n
m < n.+1 -> alpha m < alpha n.+1
have F := alpha_ltn n.
5678f17c183
F:alpha n < alpha n.+1
184
by rewrite ltnS leq_eqVlt => /orP[/eqP->| /IH /ltn_trans-> //].
Qed.

Lemma alpha_inj : injective alpha.
a4
injective alpha
Proof.
18b
move=> m n amEan; apply/eqP.
5678f17c
amEan:alpha m = alpha n
m == n
by case: ltngtP => // /alpha_mono; rewrite amEan ltnn.
Qed.

Lemma alpha_gt0 n : 0 < alpha n.
18
0 < alpha n
Proof.
196 by case: n => // n; apply: leq_ltn_trans (alpha_ltn _). Qed.

Lemma alpha_gtn_n n : n < alpha n.
18
n < alpha n
Proof.
19b by elim: n => // n IH; apply: leq_trans (alpha_ltn _). Qed.

Definition isAB i := exists m, i = a ^ m.1 * b ^ m.2.

Lemma isAB_aexp i : isAB (a ^ i).
36
isAB (a ^ i)
Proof.
1a0 by exists (i, 0); rewrite muln1. Qed.

Lemma isAB_bexp i : isAB (b ^ i).
36
isAB (b ^ i)
Proof.
1a5 by exists (0, i); rewrite mul1n. Qed.

Lemma isAB_amul i : isAB i -> isAB (a * i).
36
isAB i -> isAB (a * i)
Proof.
1aa
case=> [] [m1 m2 /= ->]; exists (m1.+1, m2).
5678f
i, m1, m2:nat
a * (a ^ m1 * b ^ m2) =
a ^ (m1.+1, m2).1 * b ^ (m1.+1, m2).2
by rewrite !mulnA expnS.
Qed.

Lemma isAB_bmul i : isAB  i-> isAB (b * i).
36
isAB i -> isAB (b * i)
Proof.
1b5
case=> [] [m1 m2 /= ->]; exists (m1, m2.+1).
1b1
b * (a ^ m1 * b ^ m2) =
a ^ (m1, m2.+1).1 * b ^ (m1, m2.+1).2
by rewrite mulnCA expnS.
Qed.

Lemma isAB_alphal n i : i \in alphal n -> isAB i.
2f
i \in alphal n -> isAB i
Proof.
1be
elim: n i => /= [i|n IH i]; rewrite ?mem_merge ?inE.
36
[|| i == 1, i == a | i == b] -> isAB i
5678f19
IH:forall i : nat, i \in alphal n -> isAB i
37
i
  \in (if a * head 1 (alphal n) \in alphal n
       then
        if b * head 1 (alphal n) \in alphal n
        then [::]
        else [:: b * head 1 (alphal n)]
       else
        a * head 1 (alphal n)
        :: (if b * head 1 (alphal n) \in alphal n
            then [::]
            else [:: b * head 1 (alphal n)])) ++
      behead (alphal n) -> isAB i
  case/or3P => /eqP->; first by exists (0, 0).
36
isAB a
36
isAB b
1c7
    by apply: (isAB_aexp 1).
36
1d1
1c6
  by apply: (isAB_bexp 1).
1c8
1ca
have F : i \in behead (alphal n) -> exists m, i = a ^ m.1 * b ^ m.2.
1c8
i \in behead (alphal n) ->
exists m : nat * nat, i = a ^ m.1 * b ^ m.2
5678f191c937
F:i \in behead (alphal n) ->
exists m : nat * nat, i = a ^ m.1 * b ^ m.2
1ca
  by move=> U; apply: IH (mem_behead _).
1de
1ca
have [[m1 m2 Hm]] : exists m, head 1 (alphal n) = a ^ m.1 * b ^ m.2.
1de
exists m : nat * nat,
  head 1 (alphal n) = a ^ m.1 * b ^ m.2
5678f191c9371df
m1, m2:nat
Hm:head 1 (alphal n) =
a ^ (m1, m2).1 * b ^ (m1, m2).2
1ca
  case: (alphal n) IH => /= [_|c l F1]; first by exists (0, 0).
5678f431dff849
F1:forall i : nat, i \in c :: l -> isAB i
exists m : nat * nat, c = a ^ m.1 * b ^ m.2
1e7
  by apply: F1; rewrite inE eqxx.
1e9
1ca
(do 2 case: (_ \in alphal _)); rewrite /= ?inE.
1e9
i \in behead (alphal n) -> isAB i
1e9
(i == b * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
1e9
(i == a * head 1 (alphal n))
|| (i \in behead (alphal n)) -> isAB i
1e9
[|| i == a * head 1 (alphal n),
    i == b * head 1 (alphal n)
  | i \in behead (alphal n)] -> isAB i
-
1f6 by apply: F.
1e9
1fb
1fc1fe
rewrite /=.
202
-
202 case/orP=> [/eqP->|/F//]; exists (m1, m2.+1).
1e9
b * head 1 (alphal n) =
a ^ (m1, m2.+1).1 * b ^ (m1, m2.+1).2
204
  by rewrite /= Hm mulnCA expnS.
1e9
1fd
1fe
-
20c case/orP=> [/eqP->|/F//]; exists (m1.+1, m2).
1e9
a * head 1 (alphal n) =
a ^ (m1.+1, m2).1 * b ^ (m1.+1, m2).2
20e
  by rewrite Hm expnS !mulnA.
1e9
1ff
case/or3P=> [/eqP->|/eqP->|//].
1e9
isAB (a * head 1 (alphal n))
1e9
isAB (b * head 1 (alphal n))
  by exists (m1.+1, m2); rewrite Hm expnS !mulnA.
1e9
21d
by exists (m1, m2.+1); rewrite /= Hm mulnCA expnS.
Qed.

Lemma isAB_alpha n : isAB (alpha n).
18
isAB (alpha n)
Proof.
222
rewrite /alpha.
18
isAB (head 1 (alphal n))
case: (alphal n) (alphal_neq_nil n) 
      (@isAB_alphal n (head 1 (alphal n))) => //= c l _.
5678f8849
(c \in c :: l -> isAB c) -> isAB c
by apply; rewrite inE eqxx.
Qed.

Lemma in_alphal n i :
 i \in alphal n -> i != alpha n -> i \in alphal n.+1.
2f
i \in alphal n -> i != alpha n -> i \in alphal n.+1
Proof.
230
have := alpha_gt0 n.
2f
0 < alpha n ->
i \in alphal n -> i != alpha n -> i \in alphal n.+1
rewrite  /alpha /= mem_merge mem_cat orbC.
2f
0 < head 1 (alphal n) ->
i \in alphal n ->
i != head 1 (alphal n) ->
(i \in behead (alphal n))
|| (i
      \in (if a * head 1 (alphal n) \in alphal n
           then
            if b * head 1 (alphal n) \in alphal n
            then [::]
            else [:: b * head 1 (alphal n)]
           else
            a * head 1 (alphal n)
            :: (if b * head 1 (alphal n) \in alphal n
                then [::]
                else [:: b * head 1 (alphal n)])))
case: (alphal n) => //= c l cP.
5678f1930f849
cP:0 < c
i \in c :: l ->
i != c ->
(i \in l)
|| (i
      \in (if a * c \in c :: l
           then
            if b * c \in c :: l
            then [::]
            else [:: b * c]
           else
            a * c
            :: (if b * c \in c :: l
                then [::]
                else [:: b * c])))
by rewrite inE => /orP[/eqP->|->//]; rewrite eqxx.
Qed.

Lemma alpha_in_alphal n : alpha n \in alphal n.
18
alpha n \in alphal n
Proof.
243
have /= := alphal_neq_nil n.
18
alphal n != [::] -> alpha n \in alphal n
rewrite /alpha; case: alphal => //= c l.
22d
true -> c \in c :: l
by rewrite inE eqxx.
Qed.

Lemma in_alphalS n i :
 i \in alphal n.+1 -> 
 i != a * alpha n ->  i != b * alpha n ->
 i \in alphal n.
2f
i \in alphal n.+1 ->
i != a * alpha n -> i != b * alpha n -> i \in alphal n
Proof.
250
rewrite /alpha /=.
2f
i
  \in merge leq
        (if a * head 1 (alphal n) \in alphal n
         then
          if b * head 1 (alphal n) \in alphal n
          then [::]
          else [:: b * head 1 (alphal n)]
         else
          a * head 1 (alphal n)
          :: (if b * head 1 (alphal n) \in alphal n
              then [::]
              else [:: b * head 1 (alphal n)]))
        (behead (alphal n)) ->
i != a * head 1 (alphal n) ->
i != b * head 1 (alphal n) -> i \in alphal n
set h := head _ _.
5678f1930e6
i
  \in merge leq
        (if a * h \in alphal n
         then
          if b * h \in alphal n
          then [::]
          else [:: b * h]
         else
          a * h
          :: (if b * h \in alphal n
              then [::]
              else [:: b * h])) (behead (alphal n)) ->
i != a * h -> i != b * h -> i \in alphal n
rewrite mem_merge mem_cat => /orP[]; last first.
25b
i \in behead (alphal n) ->
i != a * h -> i != b * h -> i \in alphal n
25b
i
  \in (if a * h \in alphal n
       then
        if b * h \in alphal n
        then [::]
        else [:: b * h]
       else
        a * h
        :: (if b * h \in alphal n
            then [::]
            else [:: b * h])) ->
i != a * h -> i != b * h -> i \in alphal n
  by case: alphal => //= c l; rewrite inE orbC => ->.
25b
263
by (do 2 case: (_ \in alphal _); rewrite //= ?inE) => 
   [/eqP->|/eqP->|/orP[/eqP->|/eqP->]]; rewrite eqxx.
Qed.

Lemma a_in_alphalS n : a * alpha n \in alphal n.+1.
18
a * alpha n \in alphal n.+1
Proof.
268
have := alpha_gt0 n.
18
0 < alpha n -> a * alpha n \in alphal n.+1
have := @in_alphal n (a * alpha n).
18
(a * alpha n \in alphal n ->
 a * alpha n != alpha n -> a * alpha n \in alphal n.+1) ->
0 < alpha n -> a * alpha n \in alphal n.+1
rewrite /alpha /= mem_merge.
18
(a * head 1 (alphal n) \in alphal n ->
 a * head 1 (alphal n) != head 1 (alphal n) ->
 a * head 1 (alphal n)
   \in (if a * head 1 (alphal n) \in alphal n
        then
         if b * head 1 (alphal n) \in alphal n
         then [::]
         else [:: b * head 1 (alphal n)]
        else
         a * head 1 (alphal n)
         :: (if b * head 1 (alphal n) \in alphal n
             then [::]
             else [:: b * head 1 (alphal n)])) ++
       behead (alphal n)) ->
0 < head 1 (alphal n) ->
a * head 1 (alphal n)
  \in (if a * head 1 (alphal n) \in alphal n
       then
        if b * head 1 (alphal n) \in alphal n
        then [::]
        else [:: b * head 1 (alphal n)]
       else
        a * head 1 (alphal n)
        :: (if b * head 1 (alphal n) \in alphal n
            then [::]
            else [:: b * head 1 (alphal n)])) ++
      behead (alphal n)
set h := head _ _.
e5
(a * h \in alphal n ->
 a * h != h ->
 a * h
   \in (if a * h \in alphal n
        then
         if b * h \in alphal n
         then [::]
         else [:: b * h]
        else
         a * h
         :: (if b * h \in alphal n
             then [::]
             else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
a * h
  \in (if a * h \in alphal n
       then
        if b * h \in alphal n
        then [::]
        else [:: b * h]
       else
        a * h
        :: (if b * h \in alphal n
            then [::]
            else [:: b * h])) ++ behead (alphal n)
have [H H1 H2|] := boolP (_ \in alphal n).
5678f19e6
H:a * h \in alphal n
H1:true ->
a * h != h ->
a * h
  \in (if b * h \in alphal n
       then [::]
       else [:: b * h]) ++ behead (alphal n)
H2:0 < h
a * h
  \in (if b * h \in alphal n then [::] else [:: b * h]) ++
      behead (alphal n)
e5
a * h \notin alphal n ->
(false ->
 a * h != h ->
 a * h
   \in (a * h
        :: (if b * h \in alphal n
            then [::]
            else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
a * h
  \in (a * h
       :: (if b * h \in alphal n
           then [::]
           else [:: b * h])) ++ behead (alphal n)
  apply: H1 => //.
5678f19e6280282
a * h != h
284
  by rewrite -{2}[h]mul1n eqn_mul2r negb_or !neq_ltn H2 aL1 !orbT.
e5
286
by rewrite mem_cat inE eqxx.
Qed.

Lemma b_in_alphalS n : b * alpha n \in alphal n.+1.
18
b * alpha n \in alphal n.+1
Proof.
290
have := alpha_gt0 n.
18
0 < alpha n -> b * alpha n \in alphal n.+1
have := @in_alphal n (b * alpha n).
18
(b * alpha n \in alphal n ->
 b * alpha n != alpha n -> b * alpha n \in alphal n.+1) ->
0 < alpha n -> b * alpha n \in alphal n.+1
rewrite /alpha /= mem_merge.
18
(b * head 1 (alphal n) \in alphal n ->
 b * head 1 (alphal n) != head 1 (alphal n) ->
 b * head 1 (alphal n)
   \in (if a * head 1 (alphal n) \in alphal n
        then
         if b * head 1 (alphal n) \in alphal n
         then [::]
         else [:: b * head 1 (alphal n)]
        else
         a * head 1 (alphal n)
         :: (if b * head 1 (alphal n) \in alphal n
             then [::]
             else [:: b * head 1 (alphal n)])) ++
       behead (alphal n)) ->
0 < head 1 (alphal n) ->
b * head 1 (alphal n)
  \in (if a * head 1 (alphal n) \in alphal n
       then
        if b * head 1 (alphal n) \in alphal n
        then [::]
        else [:: b * head 1 (alphal n)]
       else
        a * head 1 (alphal n)
        :: (if b * head 1 (alphal n) \in alphal n
            then [::]
            else [:: b * head 1 (alphal n)])) ++
      behead (alphal n)
set h := head _ _.
e5
(b * h \in alphal n ->
 b * h != h ->
 b * h
   \in (if a * h \in alphal n
        then
         if b * h \in alphal n
         then [::]
         else [:: b * h]
        else
         a * h
         :: (if b * h \in alphal n
             then [::]
             else [:: b * h])) ++ behead (alphal n)) ->
0 < h ->
b * h
  \in (if a * h \in alphal n
       then
        if b * h \in alphal n
        then [::]
        else [:: b * h]
       else
        a * h
        :: (if b * h \in alphal n
            then [::]
            else [:: b * h])) ++ behead (alphal n)
have [H H1 H2|] := boolP (b * _ \in alphal n).
5678f19e6
H:b * h \in alphal n
H1:true ->
b * h != h ->
b * h
  \in (if a * h \in alphal n
       then [::]
       else [:: a * h]) ++ behead (alphal n)
282
b * h
  \in (if a * h \in alphal n then [::] else [:: a * h]) ++
      behead (alphal n)
e5
b * h \notin alphal n ->
(false ->
 b * h != h ->
 b * h
   \in (if a * h \in alphal n
        then [:: b * h]
        else [:: a * h; b * h]) ++ behead (alphal n)) ->
0 < h ->
b * h
  \in (if a * h \in alphal n
       then [:: b * h]
       else [:: a * h; b * h]) ++ behead (alphal n)
  apply: H1 => //.
5678f19e62a8282
b * h != h
2ab
  by rewrite -{2}[h]mul1n eqn_mul2r negb_or !neq_ltn H2 bL1 !orbT.
e5
2ad
by have [] := boolP (a * _ \in alphal n); rewrite mem_cat !inE eqxx // orbT.
Qed.

Lemma alpha_surjective m n : {k | alpha k = a ^ m * b ^ n}.
17b
{k : nat | alpha k = a ^ m * b ^ n}
Proof.
2b7
pose P p := has (fun i => i %| a ^ m * b ^ n) (alphal p).
5678f17c
P:=fun p : nat =>
has (dvdn^~ (a ^ m * b ^ n)) (alphal p):nat -> bool
2b9
have F1 : exists n, P n.
2be
exists n : nat, P n
5678f17c2bf
F1:exists n : nat, P n
2b9
  by exists 0; apply/hasP; exists 1.
2c6
2b9
have F2 : 0 < a ^ m *  b ^ n.
2c6
0 < a ^ m * b ^ n
5678f17c2bf2c7
F2:0 < a ^ m * b ^ n
2b9
  rewrite muln_gt0 !expn_gt0 ?(ltn_trans _ aLb) (ltn_trans _ aL1) //.
2d1
2b9
have F3 p : P p -> p <= alpha (a ^ m * b ^ n).
5678f17c2bf2c72d2
p:nat
P p -> p <= alpha (a ^ m * b ^ n)
5678f17c2bf2c72d2
F3:forall p : nat, P p -> p <= alpha (a ^ m * b ^ n)
2b9
  move=> /hasP[q] qIa.
5678f17c2bf2c72d22da
q:nat_eqType
qIa:q \in alphal p
q %| a ^ m * b ^ n -> p <= alpha (a ^ m * b ^ n)
2dc
  suff F : alpha p <= q.
5678f17c2bf2c72d22da2e42e5
F:alpha p <= q
2e6
2e3
alpha p <= q
2dd
     move=> /(dvdn_leq F2) H.
5678f17c2bf2c72d22da2e42e52eb
H:q <= a ^ m * b ^ n
p <= alpha (a ^ m * b ^ n)
2ec
     rewrite ltnW // (leq_trans (alpha_gtn_n _)) //.
2f2
alpha p <= alpha (a ^ m * b ^ n)
2ec
     by rewrite (leq_trans F) // (leq_trans H) // ltnW // alpha_gtn_n.
2e3
2ee
2dc
  have /= := sorted_alphal p; rewrite /alpha.
2e3
sorted leq (alphal p) -> head 1 (alphal p) <= q
2dc
  case: (alphal _) qIa => //= a1 l.
5678f17c2bf2c72d22da2e4
a1:nat
49
q \in a1 :: l -> path leq a1 l -> a1 <= q
2dc
  by rewrite inE => /orP[/eqP->//|qIl /(order_path_min leq_trans) /allP/(_ _ qIl)].
2de
2b9
exists (ex_maxn F1 F3).
2de
alpha (ex_maxn F1 F3) = a ^ m * b ^ n
case: ex_maxnP => i /hasP[x xIa] Hx Fx.
5678f17c2bf2c72d22df37
x:nat_eqType
xIa:x \in alphal i
Hx:x %| a ^ m * b ^ n
Fx:forall j : nat, P j -> j <= i
alpha i = a ^ m * b ^ n
have : ~~ P i.+1 by apply/negP=> /Fx; rewrite ltnn.
310
~~ P i.+1 -> alpha i = a ^ m * b ^ n
move/hasPn => FF.
5678f17c2bf2c72d22df37311312313314
FF:{in alphal i.+1,
  forall x : nat_eqType, ~~ (x %| a ^ m * b ^ n)}
315
have F4 : x = alpha i.
31d
x = alpha i
5678f17c2bf2c72d22df3731131231331431e
F4:x = alpha i
315
  by apply/eqP; case: eqP=> // /eqP /(in_alphal xIa) /FF/negP[].
325
315
case: (isAB_alpha i) => [] [m1 n1 F5].
5678f17c2bf2c72d22df3731131231331431e326
m1, n1:nat
F5:alpha i = a ^ (m1, n1).1 * b ^ (m1, n1).2
315
have Cabe m2 n2 : coprime (a ^ m2) (b ^ n2).
5678f17c2bf2c72d22df3731131231331431e32632e32f
m2, n2:nat
coprime (a ^ m2) (b ^ n2)
5678f17c2bf2c72d22df3731131231331431e32632e32f
Cabe:forall m2 n2 : nat, coprime (a ^ m2) (b ^ n2)
315
  case: m2 => [|m2]; first by rewrite coprime1n.
5678f17c2bf2c72d22df3731131231331431e32632e32f
n2, m2:nat
coprime (a ^ m2.+1) (b ^ n2)
336
  case: n2 => [|n2]; first by rewrite coprimen1.
333
coprime (a ^ m2.+1) (b ^ n2.+1)
336
  by rewrite coprime_pexpl // coprime_pexpr.
338
315
move: Hx.
5678f17c2bf2c72d22df3731131231431e32632e32f339
x %| a ^ m * b ^ n -> alpha i = a ^ m * b ^ n
rewrite F4 F5 Gauss_dvd //=.
34a
(a ^ m1 %| a ^ m * b ^ n) && (b ^ n1 %| a ^ m * b ^ n) ->
a ^ m1 * b ^ n1 = a ^ m * b ^ n
rewrite Gauss_dvdl // Gauss_dvdr 1?coprime_sym // .
34a
(a ^ m1 %| a ^ m) && (b ^ n1 %| b ^ n) ->
a ^ m1 * b ^ n1 = a ^ m * b ^ n
rewrite !dvdn_Pexp2l //.
34a
(m1 <= m) && (n1 <= n) ->
a ^ m1 * b ^ n1 = a ^ m * b ^ n
rewrite leq_eqVlt => /andP[/orP[/eqP mEm1|H1 H2]]; last first.
5678f17c2bf2c72d22df3731131231431e32632e32f339
H1:m1 < m
H2:n1 <= n
a ^ m1 * b ^ n1 = a ^ m * b ^ n
5678f17c2bf2c72d22df3731131231431e32632e32f339
mEm1:m1 = m
n1 <= n -> a ^ m1 * b ^ n1 = a ^ m * b ^ n
  case/negP: (FF _ (a_in_alphalS _)).
35b
a * alpha i %| a ^ m * b ^ n
35f
  rewrite F5 /= mulnA -expnS.
35b
a ^ m1.+1 * b ^ n1 %| a ^ m * b ^ n
35f
  by apply: dvdn_mul; apply: dvdn_exp2l.
361
363
rewrite leq_eqVlt => /orP[/eqP nEn1 //|H1]; first by rewrite mEm1 nEn1.
5678f17c2bf2c72d22df3731131231431e32632e32f339362
H1:n1 < n
35e
case/negP: (FF _ (b_in_alphalS _)).
372
b * alpha i %| a ^ m * b ^ n
rewrite mulnC F5 mEm1 /= -mulnA -expnSr.
372
a ^ m * b ^ n1.+1 %| a ^ m * b ^ n
by apply: dvdn_mul; apply: dvdn_exp2l.
Qed.

Lemma isAB_leq_alphaSn i v : isAB v -> alpha i < v -> alpha i.+1 <= v.
5678f
i, v:nat
isAB v -> alpha i < v -> alpha i.+1 <= v
Proof.
37d
case=> [] [m1 m2 ->].
5678f
i, v, m1, m2:nat
alpha i < a ^ (m1, m2).1 * b ^ (m1, m2).2 ->
alpha i.+1 <= a ^ (m1, m2).1 * b ^ (m1, m2).2
case: (alpha_surjective m1 m2) => j <- iLj.
5678f
i, v, m1, m2, j:nat
iLj:alpha i < alpha j
alpha i.+1 <= alpha j
case: (leqP i.+1 j) => [|H].
38c
i < j -> alpha i.+1 <= alpha j
5678f38d38e
H:j < i.+1
38f
  by rewrite leq_eqVlt => /orP[/eqP->//|/alpha_mono/ltnW].
396
38f
move: H iLj; rewrite [alpha _ < _]ltnNge.
5678f38d
j < i.+1 ->
~~ (alpha j <= alpha i) -> alpha i.+1 <= alpha j
rewrite ltnS leq_eqVlt => /orP[/eqP->//|/alpha_mono/ltnW->//].
39e
~~ (alpha i <= alpha i) -> alpha i.+1 <= alpha i
by rewrite leqnn.
Qed.

Lemma alpha_leq_double i : alpha i.+1 <= a * alpha i.
36
alpha i.+1 <= a * alpha i
Proof.
3a5
apply: isAB_leq_alphaSn; first by apply/isAB_amul/isAB_alpha.
36
alpha i < a * alpha i
by rewrite -[X in X < _]mul1n ltn_mul2r alpha_gt0.
Qed.

Lemma isAB_geq_alphaSn i v : isAB v -> v < alpha i.+1 -> v <= alpha i.
37f
isAB v -> v < alpha i.+1 -> v <= alpha i
Proof.
3ae
move => isAB; have := @isAB_leq_alphaSn i _ isAB.
5678f380
isAB:Main.isAB v
(alpha i < v -> alpha i.+1 <= v) ->
v < alpha i.+1 -> v <= alpha i
by do 2 case: leqP => // _.
Qed.

Lemma sum_alpha_leq n i : 
  i <= n ->
 \sum_(j < n) alpha j <= (a * \sum_(j < (n - i)) alpha j) + \sum_(j < i) b ^ j.
42
i <= n ->
\sum_(j < n) alpha j <=
a * (\sum_(j < n - i) alpha j) + \sum_(j < i) b ^ j
Proof.
3b9
move=> iLn.
5678f43
iLn:i <= n
\sum_(j < n) alpha j <=
a * (\sum_(j < n - i) alpha j) + \sum_(j < i) b ^ j
rewrite -!(big_mkord xpredT) big_distrr /=.
3c0
\sum_(0 <= i < n) alpha i <=
\sum_(0 <= i < n - i) a * alpha i +
\sum_(0 <= i < i) b ^ i
suff aux : forall u v w n n0 n1 : nat,
           u = v + w ->
          (v != 0) * alpha n <= a * alpha n0 ->
          (w != 0) * alpha n <= b ^ n1 ->
          \sum_(n <= i0 < n + u) alpha i0 <=
          \sum_(n0 <= i < n0 + v) a * alpha i +
          \sum_(n1 <= i0 < n1 + w) b ^ i0.
5678f433c1
aux:forall u v w n n0 n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i + \sum_(n1 <= i0 < n1 + w) b ^ i0
3c6
3c0
forall u v w n n0 n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
  rewrite -{1}[n]add0n -{1}[n - i]add0n -{2}[i]add0n.
3ca
\sum_(0 <= i < 0 + n) alpha i <=
\sum_(0 <= i < 0 + (n - i)) a * alpha i +
\sum_(0 <= i < 0 + i) b ^ i
3cc
  apply: aux => //.
3c0
n = n - i + i
3c0
(n - i != 0) * alpha 0 <= a * alpha 0
3c0
(i != 0) * alpha 0 <= b ^ 0
3cd
  -
3d4 by rewrite subnK.
3c0
3d9
3da3cd
  -
3de by rewrite !muln1; apply: leq_trans aL1; case: eqP.
3c0
3db
3cc
  by rewrite muln1; case: eqP.
3c0
3ce
elim => {i iLn}[[] [] // i j k _ _| 
                     u IH [|v] [|w] // i j k uvw aM1 aM2].
5678f
n, i, j, k:nat
(0 != 0) * alpha i <= b ^ k ->
\sum_(i <= i0 < i + 0) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
5678f
n, u:nat
IH:forall v w n n0 n1 : nat,
u = v + w ->
(v != 0) * alpha n <= a * alpha n0 ->
(w != 0) * alpha n <= b ^ n1 ->
\sum_(n <= i0 < n + u) alpha i0 <=
\sum_(n0 <= i < n0 + v) a * alpha i +
\sum_(n1 <= i0 < n1 + w) b ^ i0
w, i, j, k:nat
uvw:u.+1 = 0 + w.+1
aM1:(0 != 0) * alpha i <= a * alpha j
aM2:(w.+1 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
5678f3f13f2
v, i, j, k:nat
uvw:u.+1 = v.+1 + 0
aM1:(v.+1 != 0) * alpha i <= a * alpha j
aM2:(0 != 0) * alpha i <= b ^ k
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
5678f3f13f2
v, w, i, j, k:nat
uvw:u.+1 = v.+1 + w.+1
3fc3f6
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
-
3e9 by rewrite !addn0 big_geq.
3f0
3f7
3f83ff
-
406 rewrite big_ltn; last by rewrite addnS leq_addr.
3f0
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
408
  rewrite [X in _ <= _ + X]big_ltn; last by rewrite addnS leq_addr.
3f0
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
(b ^ k + \sum_(k.+1 <= i < k + w.+1) b ^ i)
408
  rewrite addnCA.
3f0
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
b ^ k +
(\sum_(j <= i < j + 0) a * alpha i +
 \sum_(k.+1 <= i < k + w.+1) b ^ i)
408
  apply: leq_add; first by rewrite mul1n in aM2.
3f0
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k.+1 <= i < k + w.+1) b ^ i
408
  rewrite -!addSnnS.
3f0
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j <= i < j + 0) a * alpha i +
\sum_(k.+1 <= i < k.+1 + w) b ^ i
408
  apply: IH => //; first by case: uvw.
5678f
n, u, w, i, j, k:nat
3f43f53f6
(w != 0) * alpha i.+1 <= b ^ k.+1
408
  case: (w) => // w1 //.
5678f4223f43f53f6
w1:nat
(w1.+1 != 0) * alpha i.+1 <= b ^ k.+1
408
  rewrite !mul1n in aM2 |- *.
5678f4223f43f5428
aM2:alpha i <= b ^ k
alpha i.+1 <= b ^ k.+1
408
  suff /leq_trans-> : alpha i.+1 <= a * alpha i => //.
42d
a * alpha i <= b ^ k.+1
42d
3a7
3f83ff
    by rewrite expnS; apply: leq_mul => //; apply: ltnW.
42d
3a7
408
  by apply: alpha_leq_double.
3f9
3fe
3ff
-
43a rewrite big_ltn; last by rewrite addnS leq_addr.
3f9
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
43c
  rewrite [X in _ <= X + _]big_ltn; last by rewrite addnS leq_addr.
3f9
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j + \sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
43c
  rewrite -addnA.
3f9
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j +
(\sum_(j.+1 <= i < j + v.+1) a * alpha i +
 \sum_(k <= i0 < k + 0) b ^ i0)
43c
  apply: leq_add; first by rewrite mul1n in aM1.
3f9
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
43c
  rewrite -!addSnnS.
3f9
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j.+1 <= i < j.+1 + v) a * alpha i +
\sum_(k <= i0 < k + 0) b ^ i0
43c
  apply: IH => //; first by case: uvw.
5678f
n, u, v, i, j, k:nat
3fb3fc3fd
(v != 0) * alpha i.+1 <= a * alpha j.+1
43c
  case: (v) => // v1 //.
5678f4563fb3fc3fd
v1:nat
(v1.+1 != 0) * alpha i.+1 <= a * alpha j.+1
43c
  rewrite !mul1n in aM1 |- *.
5678f4563fb3fd45c
aM1:alpha i <= a * alpha j
alpha i.+1 <= a * alpha j.+1
43c
  apply: isAB_leq_alphaSn; first by apply/isAB_amul/isAB_alpha.
461
alpha i < a * alpha j.+1
43c
  apply: leq_ltn_trans aM1 _.
5678f4563fb3fd45c
a * alpha j < a * alpha j.+1
43c
  by rewrite ltn_mul2l ltnW // alpha_ltn.
400
403
have aM3 : alpha i.+1 <= a * alpha j.+1.
400
463
5678f3f13f24014023fc3f6
aM3:alpha i.+1 <= a * alpha j.+1
403
  rewrite !mul1n in aM1.
5678f3f13f24014023f6462
463
473
  apply: isAB_leq_alphaSn; first by apply/isAB_amul/isAB_alpha.
47a
467
473
  apply: leq_ltn_trans aM1 _.
5678f3f13f24014023f6
46c
473
  by rewrite ltn_mul2l ltnW // alpha_ltn.
475
403
case: (leqP (a * alpha j) (b ^ k)) => [|bLaa].
475
a * alpha j <= b ^ k ->
\sum_(i <= i1 < i + u.+1) alpha i1 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i1 < k + w.+1) b ^ i1
5678f3f13f24014023fc3f6476
bLaa:b ^ k < a * alpha j
403
-
486 rewrite leq_eqVlt => /orP[/eqP aaEb |aaLb].
5678f3f13f24014023fc3f6476
aaEb:a * alpha j = b ^ k
403
5678f3f13f24014023fc3f6476
aaLb:a * alpha j < b ^ k
403
48a
  have : a %| b ^ k by rewrite -aaEb dvdn_mulr.
491
a %| b ^ k ->
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
493
  move/gcdn_idPl.
491
gcdn a (b ^ k) = a ->
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
493
  have /eqP-> := coprimeXr k aCb.
491
1 = a ->
\sum_(i <= i0 < i + u.+1) alpha i0 <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
493
  by case: a aL1 => // [] [].
495
403
489
-
4a4 rewrite big_ltn; last by rewrite addnS leq_addr.
495
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
489
  rewrite [X in _ <= X + _]big_ltn; last by rewrite addnS leq_addr.
495
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j + \sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
489
  rewrite -addnA.
495
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
a * alpha j +
(\sum_(j.+1 <= i < j + v.+1) a * alpha i +
 \sum_(k <= i0 < k + w.+1) b ^ i0)
489
  apply: leq_add; first by rewrite mul1n in aM1.
495
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j.+1 <= i < j + v.+1) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
489
  rewrite -2!addSnnS.
495
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j.+1 <= i < j.+1 + v) a * alpha i +
\sum_(k <= i0 < k + w.+1) b ^ i0
489
  apply: IH => //; first by case: uvw.
5678f
n, u, v, w, i, j, k:nat
4023fc3f6476496
457
4be
(w.+1 != 0) * alpha i.+1 <= b ^ k
48a
    case: (v) => // v1 //.
5678f4bf4023fc3f647649645c
45d
4c0
    by rewrite !mul1n.
4be
4c2
489
  rewrite !mul1n in aM1, aM2 |- *.
5678f4bf40247649646242e
alpha i.+1 <= b ^ k
489
  apply: isAB_leq_alphaSn (isAB_bexp _) _.
4cd
alpha i < b ^ k
489
  by apply: leq_ltn_trans aaLb.
48b
403
rewrite big_ltn; last by rewrite addnS leq_addr.
48b
4aa
rewrite [X in _ <= _ + X]big_ltn; last by rewrite addnS leq_addr.
48b
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
(b ^ k + \sum_(k.+1 <= i < k + w.+1) b ^ i)
rewrite addnCA.
48b
alpha i + \sum_(i.+1 <= i < i + u.+1) alpha i <=
b ^ k +
(\sum_(j <= i < j + v.+1) a * alpha i +
 \sum_(k.+1 <= i < k + w.+1) b ^ i)
apply: leq_add; first by rewrite mul1n in aM2.
48b
\sum_(i.+1 <= i < i + u.+1) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k.+1 <= i < k + w.+1) b ^ i
rewrite -addSnnS -(addSnnS k).
48b
\sum_(i.+1 <= i < i.+1 + u) alpha i <=
\sum_(j <= i < j + v.+1) a * alpha i +
\sum_(k.+1 <= i < k.+1 + w) b ^ i
apply: IH => //; first by move: uvw; rewrite addnS => [[]].
5678f4bf4023fc3f647648c
(v.+1 != 0) * alpha i.+1 <= a * alpha j
4ec
423
  rewrite !mul1n in aM1, aM2 |- *.
5678f4bf40247648c46242e
alpha i.+1 <= a * alpha j
4ee
  apply: isAB_leq_alphaSn.
4f3
isAB (a * alpha j)
4f3
alpha i < a * alpha j
4ef
    by apply: isAB_amul; apply: isAB_alpha.
4f3
4fb
4ee
  by apply: leq_ltn_trans bLaa.
4ec
423
case: (w) => // w1.
5678f4bf4023fc3f647648c428
429
rewrite !mul1n in aM1, aM2 |- *.
5678f4bf40247648c42846242e
42f
apply: isAB_leq_alphaSn (isAB_bexp _) _.
509
alpha i < b ^ k.+1
apply: leq_ltn_trans aM2 _.
5678f4bf40247648c428462
b ^ k < b ^ k.+1
by rewrite ltn_exp2l.
Qed.

Lemma alpha0 : alpha 0 = 1.
a4
alpha 0 = 1
Proof.
514 by []. Qed.

Lemma alpha1 : alpha 1 = a.
a4
alpha 1 = a
Proof.
519 
by rewrite /alpha /= !ifT //= muln1 !inE eqxx ?orbT.
Qed.

Lemma b_exp_leq k n : b ^ k <= alpha n -> k <= n.
5678f
k, n:nat
b ^ k <= alpha n -> k <= n
Proof.
51e
elim: n k => [k|n IH [|k Hk]//].
5678f
k:nat
b ^ k <= alpha 0 -> k <= 0
5678f19
IH:forall k : nat, b ^ k <= alpha n -> k <= n
528
Hk:b ^ k.+1 <= alpha n.+1
k < n.+1
  by rewrite -[alpha 0]/(b ^ 0) leq_exp2l.
52c
52f
apply/IH/(isAB_geq_alphaSn (isAB_bexp _)).
52c
b ^ k < alpha n.+1
by apply: leq_trans Hk; rewrite ltn_exp2l.
Qed.

Lemma alpha_exp_bound n : alpha n < b ^ n.+1.
18
alpha n < b ^ n.+1
Proof.
538 by rewrite ltnNge; apply/negP => /b_exp_leq; rewrite ltnn. Qed.

Lemma b_exp_ltn k n : b ^ k < alpha n -> k < n.
520
b ^ k < alpha n -> k < n
Proof.
53d
case: n => [|n H]; first by rewrite ltnNge expn_gt0 (leq_trans _ bL1).
5678f521
H:b ^ k < alpha n.+1
52f
by rewrite ltnS; apply/b_exp_leq/(isAB_geq_alphaSn (isAB_bexp _)).
Qed.

Lemma alpha_b_eq n i : 
   b ^ i < alpha n.+1 < b ^ i.+1 -> alpha n.+1 = a * alpha (n - i).
42
b ^ i < alpha n.+1 < b ^ i.+1 ->
alpha n.+1 = a * alpha (n - i)
Proof.
547
move=> /andP[beLa aLbe].
5678f43
beLa:b ^ i < alpha n.+1
aLbe:alpha n.+1 < b ^ i.+1
alpha n.+1 = a * alpha (n - i)
have iLm : i <= n.
54e
i <= n
5678f4354f550
iLm:i <= n
551
  apply/b_exp_leq/isAB_geq_alphaSn => //.
54e
1a7
556
  by exists (0, i); rewrite mul1n.
558
551
have [[[|x] y] Hxy] : isAB (alpha n.+1) by apply: isAB_alpha.
5678f4354f550559
y:nat
Hxy:alpha n.+1 = a ^ (0, y).1 * b ^ (0, y).2
551
5678f4354f550559
x, y:nat
Hxy:alpha n.+1 = a ^ (x.+1, y).1 * b ^ (x.+1, y).2
551
  move: beLa aLbe; rewrite Hxy.
5678f43559564565
b ^ i < a ^ (0, y).1 * b ^ (0, y).2 ->
a ^ (0, y).1 * b ^ (0, y).2 < b ^ i.+1 ->
a ^ (0, y).1 * b ^ (0, y).2 = a * alpha (n - i)
566
  rewrite mul1n !(ltn_exp2l _ _ bL1) ltnS.
56e
i < (0, y).2 ->
(0, y).2 <= i -> b ^ (0, y).2 = a * alpha (n - i)
566
  by case: leqP.
568
551
case: (alpha_surjective x y) => k Hk.
5678f4354f55055956956a528
Hk:alpha k = a ^ x * b ^ y
551
pose la := [seq alpha (j : 'I_n.+2) | j <- enum 'I_n.+2].
5678f4354f55055956956a52857b
la:=[seq alpha (j : 'I_n.+2) | j <- enum 'I_n.+2]:seq nat
551
pose lb := [seq b ^ (j : 'I_ i.+1) | j <- enum 'I_i.+1].
5678f4354f55055956956a52857b580
lb:=[seq b ^ (j : 'I_i.+1) | j <- enum 'I_i.+1]:seq nat
551
pose lc := [seq a * alpha (j : 'I_(n - i)) | j <- enum 'I_(n- i)].
5678f4354f55055956956a52857b580585
lc:=[seq a * alpha (j : 'I_(n - i))
   | j <- enum 'I_(n - i)]:seq nat
551
have Ula : uniq la.
589
uniq la
5678f4354f55055956956a52857b58058558a
Ula:uniq la
551
  rewrite map_inj_uniq; first by apply: enum_uniq.
589
injective (fun j : 'I_n.+2 => alpha j)
58f
  move=> k1 k2 H.
5678f4354f55055956956a52857b58058558a
k1, k2:ordinal_eqType n.+2
H:alpha k1 = alpha k2
k1 = k2
58f
  case: (leqP k1 k2)=> [|/alpha_mono]; last by rewrite H ltnn.
59a
k1 <= k2 -> k1 = k2
58f
  by rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono]; rewrite H ltnn.
591
551
have Sla : size la = n.+2 by rewrite size_map size_enum_ord.
5678f4354f55055956956a52857b58058558a592
Sla:size la = n.+2
551
pose la1:= [seq x <- la | a %| x].
5678f4354f55055956956a52857b58058558a5925a9
la1:=[seq x <- la | a %| x]:seq nat
551
pose la2 := [seq x <- la | ~~ (a %| x)].
5678f4354f55055956956a52857b58058558a5925a95ae
la2:=[seq x <- la | ~~ (a %| x)]:seq nat
551
pose lk := [seq a * alpha (j : 'I_k.+1) | j <- enum 'I_k.+1].
5678f4354f55055956956a52857b58058558a5925a95ae5b3
lk:=[seq a * alpha (j : 'I_k.+1) | j <- enum 'I_k.+1]:seq nat
551
have Slk : size lk = k.+1 by rewrite size_map size_enum_ord.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b8
Slk:size lk = k.+1
551
have lkEla1 : lk =i la1.
5bc
lk =i la1
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd
lkEla1:lk =i la1
551
  move=> u; rewrite mem_filter.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd
u:nat_eqType
(u \in lk) = (a %| u) && (u \in la)
5c2
  apply/mapP/idP.
5c9
(exists2 x : ordinal_eqType k.+1,
   x \in enum 'I_k.+1 & u = a * alpha x) ->
(a %| u) && (u \in la)
5c9
(a %| u) && (u \in la) ->
exists2 x : ordinal_eqType k.+1,
  x \in enum 'I_k.+1 & u = a * alpha x
5c3
    case => z Hz ->; rewrite dvdn_mulr //=.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca
z:ordinal_eqType k.+1
Hz:z \in enum 'I_k.+1
a * alpha z \in la
5d0
    have [[x1 y1] Hx1y1] : isAB (alpha z) by apply: isAB_alpha.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca5d75d8
x1, y1:nat
Hx1y1:alpha z = a ^ (x1, y1).1 * b ^ (x1, y1).2
5d9
5d0
    case: (alpha_surjective x1.+1 y1) => t Ht.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca5d75d85de5df
t:nat
Ht:alpha t = a ^ x1.+1 * b ^ y1
5d9
5d0
    suff H1t : t < n.+2.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca5d75d85de5df5e45e5
H1t:t < n.+2
5d9
5e3
t < n.+2
5d15c3
      apply/mapP; exists (Ordinal H1t); first by rewrite mem_enum.
5e9
a * alpha z = alpha (Ordinal H1t)
5eb
      by rewrite Ht expnS -mulnA -Hx1y1.
5e3
5ed
5d0
    case: leqP => // /alpha_mono.
5e3
alpha n.+1 < alpha t -> false
5d0
    rewrite ltnNge Hxy Ht /= !expnS -!mulnA -Hx1y1 -Hk.
5e3
~~ (a * alpha z <= a * alpha k) -> false
5d0
    rewrite  (leq_pmul2l (ltnW aL1)).
5e3
~~ (alpha z <= alpha k) -> false
5d0
    have : z < k.+1 by [].
5e3
z < k.+1 -> ~~ (alpha z <= alpha k) -> false
5d0
    by rewrite ltnS leq_eqVlt => /orP[/eqP->|/alpha_mono/ltnW->]; rewrite // leqnn.
5c9
5d2
5c2
  rewrite andbC => /andP[/mapP[v Hv ->] Ha].
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca
v:ordinal_eqType n.+2
Hv:v \in enum 'I_n.+2
Ha:a %| alpha v
exists2 x : ordinal_eqType k.+1,
  x \in enum 'I_k.+1 & alpha v = a * alpha x
5c2
  have [[[|x1] y1] Hx1y1] : isAB (alpha v) by apply: isAB_alpha.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca60c60d60e
y1:nat
Hx1y1:alpha v = a ^ (0, y1).1 * b ^ (0, y1).2
60f
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca60c60d60e5de
Hx1y1:alpha v =
a ^ (x1.+1, y1).1 * b ^ (x1.+1, y1).2
60f
5c3
    move: Ha; rewrite Hx1y1 mul1n /= => /gcdn_idPl.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca60c60d614615
gcdn a (b ^ y1) = a ->
exists2 x : 'I_k.+1,
  x \in enum 'I_k.+1 & b ^ y1 = a * alpha x
616
    have /eqP-> : coprime a (b ^ y1) by rewrite coprimeXr.
61d
1 = a ->
exists2 x : 'I_k.+1,
  x \in enum 'I_k.+1 & b ^ y1 = a * alpha x
616
    by move=> H; move: aL1; rewrite H ltnn.
618
60f
5c2
  case: (alpha_surjective x1 y1) => j1 Hj1.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca60c60d60e5de619
j1:nat
Hj1:alpha j1 = a ^ x1 * b ^ y1
60f
5c2
  suff H1j1 : j1 < k.+1.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5ca60c60d60e5de61962a62b
H1j1:j1 < k.+1
60f
629
j1 < k.+1
5c3
    exists (Ordinal H1j1); first by rewrite mem_enum.
62f
alpha v = a * alpha (Ordinal H1j1)
631
    by rewrite Hx1y1 expnS -mulnA Hj1.
629
633
5c2
  case: leqP => // /alpha_mono.
629
alpha k < alpha j1 -> false
5c2
  rewrite  -(ltn_pmul2l (ltnW aL1)) Hk Hj1 !mulnA -!expnS -Hxy -Hx1y1.
629
alpha n.+1 < alpha v -> false
5c2
  rewrite ltnNge isAB_geq_alphaSn //; first by apply: isAB_alpha.
629
alpha v < alpha n.+2
5c2
  by apply: alpha_mono.
5c4
551
have lbEla2 : lb =i la2.
5c4
lb =i la2
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c5
lbEla2:lb =i la2
551
  move=> u; apply/idP/idP; last first.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca
u \in la2 -> u \in lb
655
u \in lb -> u \in la2
64f
    rewrite mem_filter andbC => /andP[/mapP[v Hx ->]].
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca60c
Hx:v \in enum 'I_n.+2
~~ (a %| alpha v) -> alpha v \in lb
657
    have /alpha_mono : v < n.+2 by [].
65d
alpha v < alpha n.+2 ->
~~ (a %| alpha v) -> alpha v \in lb
657
      case: (isAB_alpha v) => [] [[|u1] v1]->/=; last first.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca60c65e
u1, v1:nat
a ^ u1.+1 * b ^ v1 < alpha n.+2 ->
~~ (a %| a ^ u1.+1 * b ^ v1) ->
a ^ u1.+1 * b ^ v1 \in lb
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca60c65e45c
a ^ 0 * b ^ v1 < alpha n.+2 ->
~~ (a %| a ^ 0 * b ^ v1) -> a ^ 0 * b ^ v1 \in lb
65864f
      by rewrite expnS -mulnA dvdn_mulr.
66c
66d
657
    rewrite mul1n => H _.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca60c65e45c
H:b ^ v1 < alpha n.+2
b ^ v1 \in lb
657
    have /(ltn_pexp2l (ltnW bL1)) v1Li : b ^ v1 < b ^ i.+1.
674
b ^ v1 < b ^ i.+1
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca60c65e45c675
v1Li:v1 < i.+1
676
65864f
      apply: leq_ltn_trans aLbe.
5678f4354f55956956a52857b58058558a5925a95ae5b35b85bd5c55ca60c65e45c675
b ^ v1 <= alpha n.+1
67b
      by apply: isAB_geq_alphaSn (isAB_bexp _) _.
67d
676
657
    by apply/mapP; exists (Ordinal v1Li); rewrite // mem_enum.
655
659
64e
  move=> /mapP[u1 _ ->].
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca
u1:ordinal_eqType i.+1
b ^ u1 \in la2
64e
  rewrite mem_filter; apply/andP; split.
68d
~~ (a %| b ^ u1)
68d
b ^ u1 \in la
64f
    apply/negP=> /gcdn_idPl.
68d
gcdn a (b ^ u1) = a -> False
694
    have /eqP-> : coprime a (b ^ u1) by rewrite coprimeXr.
68d
1 = a -> False
694
    by move=> H; move: aL1; rewrite H ltnn.
68d
696
64e
   case: (alpha_surjective 0 u1) => j1; rewrite mul1n => Hj1.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca68e62a
Hj1:alpha j1 = b ^ u1
696
64e
  suff j1Ln : j1 < n.+2.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c55ca68e62a6a6
j1Ln:j1 < n.+2
696
6a5
j1 < n.+2
64f
    by apply/mapP; exists (Ordinal j1Ln); rewrite ?mem_enum.
6a5
6ae
64e
  case: leqP => // /alpha_mono; rewrite ltnNge => /negP[].
6a5
alpha j1 <= alpha n.+1
64e
  apply: leq_trans (ltnW beLa).
6a5
alpha j1 <= b ^ i
64e
  by rewrite Hj1 leq_exp2l // -ltnS.
650
551
rewrite Hxy expnS -mulnA -Hk.
650
a * alpha k = a * alpha (n - i)
congr (_ * alpha _).
650
k = n - i
rewrite -subSS -subSS -Sla (_ : size la = size la1 + size la2); last first.
650
size la = size la1 + size la2
650
k = size la1 + size la2 - i.+2
  by rewrite !size_filter count_predC.
650
6cb
have : uniq la1.
650
uniq la1
650
uniq la1 -> k = size la1 + size la2 - i.+2
  apply: filter_uniq.
650
58e
6d3
  rewrite map_inj_uniq; first by apply: enum_uniq.
650
596
6d3
  move=> k1 k2 H.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c565159b59c
59d
6d3
  case: (leqP k1 k2)=> [|/alpha_mono]; last by rewrite H ltnn.
6df
5a1
6d3
  by rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono]; rewrite H ltnn.
650
6d5
rewrite (uniq_size_uniq _ lkEla1) => [/eqP->|]; last first.
650
uniq lk
650
k = size lk + size la2 - i.+2
  rewrite map_inj_uniq; first by apply: enum_uniq.
650
injective (fun j : 'I_k.+1 => a * alpha j)
6ea
  move=> k1 k2 H.
5678f4354f55055956956a52857b58058558a5925a95ae5b35b85bd5c5651
k1, k2:ordinal_eqType k.+1
H:a * alpha k1 = a * alpha k2
59d
6ea
  case: (leqP k1 k2)=> [|/alpha_mono]; last first.
6f4
alpha k2 < alpha k1 -> k1 = k2
6f4
5a1
6eb
    by rewrite -(ltn_pmul2l (ltnW aL1)) H ltnn.
6f4
5a1
6ea
  rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono].
6f4
alpha k1 < alpha k2 -> k1 = k2
6ea
  by rewrite -(ltn_pmul2l (ltnW aL1)) H ltnn.
650
6ec
rewrite Slk.
650
k = k.+1 + size la2 - i.+2
have : uniq la2.
650
uniq la2
650
uniq la2 -> k = k.+1 + size la2 - i.+2
  apply: filter_uniq.
6d870f
  rewrite map_inj_uniq; first by apply: enum_uniq.
6db70f
  move=> k1 k2 H.
6de70f
  case: (leqP k1 k2)=> [|/alpha_mono]; last by rewrite H ltnn.
6e270f
  by rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono]; rewrite H ltnn.
650
711
rewrite (uniq_size_uniq _ lbEla2) => [/eqP->|]; last first.
650
uniq lb
650
k = k.+1 + size lb - i.+2
  rewrite map_inj_uniq; first by apply: enum_uniq.
650
injective (fun j : 'I_i.+1 => b ^ j)
721
  by move=> k1 k2 /eqP; rewrite eqn_exp2l => // /val_eqP.
650
723
rewrite size_map size_enum_ord.
650
k = k.+1 + i.+1 - i.+2
by rewrite subSS addnK.
Qed.

Lemma sum_alpha_eq n i : 
 b ^ i <= alpha n < b ^ i.+1 ->
 \sum_(i0 < n.+1) alpha i0 =
  (a * \sum_(i0 < (n - i)) alpha i0) + \sum_(i0 < i.+1) b ^ i0.
42
b ^ i <= alpha n < b ^ i.+1 ->
\sum_(i0 < n.+1) alpha i0 =
a * (\sum_(i0 < n - i) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
Proof.
730
elim: n i => [i|n IH i].
36
b ^ i <= alpha 0 < b ^ i.+1 ->
\sum_(i0 < 1) alpha i0 =
a * (\sum_(i0 < 0 - i) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
5678f19
IH:forall i : nat,
b ^ i <= alpha n < b ^ i.+1 ->
\sum_(i0 < n.+1) alpha i0 =
a * (\sum_(i0 < n - i) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
37
b ^ i <= alpha n.+1 < b ^ i.+1 ->
\sum_(i0 < n.+2) alpha i0 =
a * (\sum_(i0 < n.+1 - i) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
  case: i => [_|i]; last by rewrite leqNgt alpha0 (ltn_exp2l 0).
a4
\sum_(i0 < 1) alpha i0 =
a * (\sum_(i0 < 0 - 0) alpha i0) +
\sum_(i0 < 1) b ^ i0
738
  by rewrite !big_ord_recr !big_ord0 muln0.
73a
73c
rewrite leq_eqVlt => /andP[/orP[/eqP Ha Hb| Ha Hb]].
5678f1973b37
Ha:b ^ i = alpha n.+1
Hb:alpha n.+1 < b ^ i.+1
\sum_(i0 < n.+2) alpha i0 =
a * (\sum_(i0 < n.+1 - i) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
5678f1973b37
Ha:b ^ i < alpha n.+1
749
74a
  case: i Ha Hb => [H|i Ha Hb].
5678f1973b
H:b ^ 0 = alpha n.+1
alpha n.+1 < b ^ 1 ->
\sum_(i0 < n.+2) alpha i0 =
a * (\sum_(i0 < n.+1 - 0) alpha i0) +
\sum_(i0 < 1) b ^ i0
5678f1973b37
Ha:b ^ i.+1 = alpha n.+1
Hb:alpha n.+1 < b ^ i.+2
\sum_(i0 < n.+2) alpha i0 =
a * (\sum_(i0 < n.+1 - i.+1) alpha i0) +
\sum_(i0 < i.+2) b ^ i0
74c
    have : alpha 0 < alpha n.+1 by apply: alpha_mono.
752
alpha 0 < alpha n.+1 ->
alpha n.+1 < b ^ 1 ->
\sum_(i0 < n.+2) alpha i0 =
a * (\sum_(i0 < n.+1 - 0) alpha i0) +
\sum_(i0 < 1) b ^ i0
755
    by rewrite [alpha 0]H ltnn.
757
75a
74b
  rewrite big_ord_recr [X in _ = _ + X]big_ord_recr /= Ha.
757
\sum_(i < n.+1) alpha i + alpha n.+1 =
a * (\sum_(i0 < n.+1 - i.+1) alpha i0) +
(\sum_(i0 < i.+1) b ^ i0 + alpha n.+1)
74b
  rewrite addnA; congr (_ + _).
757
\sum_(i < n.+1) alpha i =
a * (\sum_(i0 < n.+1 - i.+1) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
74b
  rewrite subSS.
757
\sum_(i < n.+1) alpha i =
a * (\sum_(i0 < n - i) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
74b
  apply: IH => //.
5678f43758759
b ^ i <= alpha n < b ^ i.+1
74b
  rewrite Ha alpha_ltn andbT.
771
b ^ i <= alpha n
74b
  apply: isAB_geq_alphaSn (isAB_bexp _) _.
771
b ^ i < alpha n.+1
74b
  by rewrite -Ha ltn_exp2l.
74d
74a
rewrite subSn; last exact: b_exp_ltn Ha.
74d
\sum_(i0 < n.+2) alpha i0 =
a * (\sum_(i0 < (n - i).+1) alpha i0) +
\sum_(i0 < i.+1) b ^ i0
rewrite big_ord_recr [X in _ = _  * X + _]big_ord_recr.
74d
addn_monoid
  (\big[addn_monoid/0]_(i < n.+1) alpha
                                    (widen_ord
                                       (leqnSn n.+1) i))
  (alpha ord_max) =
a *
addn_monoid
  (\big[addn_monoid/0]_(i0 < n - i) alpha
                                      (widen_ord
                                         (leqnSn
                                            (n - i))
                                         i0))
  (alpha ord_max) + \sum_(i0 < i.+1) b ^ i0
rewrite mulnDr addnAC.
74d
addn_monoid
  (\big[addn_monoid/0]_(i < n.+1) alpha
                                    (widen_ord
                                       (leqnSn n.+1) i))
  (alpha ord_max) =
a *
\big[addn_monoid/0]_(i0 < n - i) alpha
                                   (widen_ord
                                      (leqnSn (n - i))
                                      i0) +
\sum_(i0 < i.+1) b ^ i0 + a * alpha ord_max
congr (_ + _); last first.
74d
alpha ord_max = a * alpha ord_max
74d
\big[addn_monoid/0]_(i < n.+1) alpha
                                 (widen_ord
                                    (leqnSn n.+1) i) =
a *
\big[addn_monoid/0]_(i0 < n - i) alpha
                                   (widen_ord
                                      (leqnSn (n - i))
                                      i0) +
\sum_(i0 < i.+1) b ^ i0
  by apply: alpha_b_eq; rewrite ?Ha.
74d
790
apply: IH.
5678f4374e749
772
rewrite (isAB_geq_alphaSn (isAB_bexp _)) //.
797
true && (alpha n < b ^ i.+1)
apply: leq_trans Hb.
5678f4374e
alpha n < (alpha n.+1).+1
by rewrite ltnS ltnW // alpha_ltn.
Qed.

End Main.

Section S23.

Local Notation α := (alpha 2 3).

(* First 60 element of the list *)
Compute map α (iota 0 60).
= [:: 1; 2; 3; 4; 6; 8; 9; 12; 16; 18; 24; 27;
      32; 36; 48; 54; 64; 72; 81; 96; 108; 128;
      144; 162; 192; 216; 243; 256; 288; 324;
      384; 432; 486; 512; 576; 648; 729; 768;
      864; 972; 1024; 1152; 1296; 1458; 1536;
      1728; 1944; 2048; 2187; 2304; 2592; 2916;
      3072; 3456; 3888; 4096; 4374; 4608; 5184;
      5832]
: seq nat

Definition dsum_alpha n := \sum_(i < n) α i.

Local Notation S1 := dsum_alpha.

Lemma dsum_alpha_0 : S1 0 = 0.
S1 0 = 0
Proof.
7a3 by rewrite /S1 big_ord0 // =>  [] []. Qed.

Lemma dsum_alpha_1 : S1 1 = 1.
S1 1 = 1
Proof.
7a8 by rewrite /S1 big_ord_recr /= big_ord0. Qed.

Lemma div2K n : ~~ odd n -> n./2.*2 = n.
19
~~ odd n -> (n./2).*2 = n
Proof.
7ad by move=> nO; rewrite -{2}(odd_double_half n) (negPf nO). Qed.

Lemma S1_leq n i : i <= n -> S1 n <= (S1 (n - i)).*2 + (3 ^ i).-1./2.
43
i <= n -> S1 n <= (S1 (n - i)).*2 + ((3 ^ i).-1)./2
Proof.
7b3
move=> iLn.
433c1
S1 n <= (S1 (n - i)).*2 + ((3 ^ i).-1)./2
rewrite -leq_double doubleD div2K; last first.
7bb
~~ odd (3 ^ i).-1
7bb
(S1 n).*2 <= ((S1 (n - i)).*2).*2 + (3 ^ i).-1
  by rewrite -subn1 oddB ?expn_gt0 //= oddX orbT.
7bb
7c3
rewrite -!mul2n predn_exp.
7bb
2 * S1 n <=
2 * (2 * S1 (n - i)) + 3.-1 * (\sum_(i0 < i) 3 ^ i0)
rewrite -mulnDr leq_mul2l /=.
7bb
S1 n <= 2 * S1 (n - i) + \sum_(i0 < i) 3 ^ i0
by apply: sum_alpha_leq.
Qed.

Lemma log3_proof n : exists i, n  < 3 ^ i.
7af
exists i : nat, n < 3 ^ i
Proof.
7d0 by exists n; apply: ltn_expl. Qed.

Definition log3 k := (ex_minn (log3_proof k)).-1.

Lemma log30 : log3 0 = 0.
log3 0 = 0
Proof.
7d5
by rewrite /log3; case: ex_minnP => [] [|m] //= _ /(_ 0 isT); case: m.
Qed.

Lemma log31 : log3 1 = 0.
log3 1 = 0
Proof.
7da
by rewrite /log3; case: ex_minnP => [] [|m] //= _  /(_ 1 isT); case: m.
Qed. 

Lemma gtn_log3 n : n < 3 ^ (log3 n).+1.
7af
n < 3 ^ (log3 n).+1
Proof.
7df
rewrite /log3; case: ex_minnP => [] [|m] //= nLm H.
19
nLm:n < 3 ^ 0
H:forall n0 : nat, n < 3 ^ n0 -> 0 <= n0
n < 3 ^ 1
by apply: leq_trans nLm _.
Qed.

Lemma leq_log3 n : 0 < n -> 3 ^ (log3 n) <= n.
7af
0 < n -> 3 ^ log3 n <= n
Proof.
7eb
rewrite /log3; case: ex_minnP => [] [|m] //= nLm H nL.
n, m:nat
nLm:n < 3 ^ m.+1
H:forall n0 : nat, n < 3 ^ n0 -> m < n0
nL:0 < n
3 ^ m <= n
by rewrite leqNgt; apply/negP => /H; rewrite ltnn.
Qed.

Lemma leq_log3_alpha n : log3 (α n) < n.+1.
7af
log3 (α n) < n.+1
Proof.
7f9
rewrite -(ltn_exp2l _ _ (_ : 1 < 3)) //.
7af
3 ^ log3 (α n) < 3 ^ n.+1
apply: leq_ltn_trans (leq_log3 _) _; first by apply: alpha_gt0.
7af
α n < 3 ^ n.+1
by apply: alpha_exp_bound.
Qed.

Lemma S1_eq n : 0 < n -> 
  S1 n = (S1 (n - (log3 (α n.-1)).+1)).*2 + (3 ^ (log3 (α n.-1)).+1).-1./2.
7af
0 < n ->
S1 n =
(S1 (n - (log3 (α n.-1)).+1)).*2 +
((3 ^ (log3 (α n.-1)).+1).-1)./2
Proof.
806
case: n => // n _.
7af
S1 n.+1 =
(S1 (n.+1 - (log3 (α n.+1.-1)).+1)).*2 +
((3 ^ (log3 (α n.+1.-1)).+1).-1)./2
apply: double_inj.
7af
(S1 n.+1).*2 =
((S1 (n.+1 - (log3 (α n.+1.-1)).+1)).*2 +
 ((3 ^ (log3 (α n.+1.-1)).+1).-1)./2).*2
rewrite doubleD div2K; last first.
7af
~~ odd (3 ^ (log3 (α n.+1.-1)).+1).-1
7af
(S1 n.+1).*2 =
((S1 (n.+1 - (log3 (α n.+1.-1)).+1)).*2).*2 +
(3 ^ (log3 (α n.+1.-1)).+1).-1
  by rewrite -subn1 oddB ?expn_gt0 //= oddX orbT.
7af
818
rewrite -!mul2n predn_exp -mulnDr; congr (2 * _).
7af
S1 n.+1 =
2 * S1 (n.+1 - (log3 (α n.+1.-1)).+1) +
\sum_(i < (log3 (α n.+1.-1)).+1) 3 ^ i
have iLn : 3 ^ (log3 (α n)) <= α n < 3 ^ (log3 (α n)).+1.
7af
3 ^ log3 (α n) <= α n < 3 ^ (log3 (α n)).+1
19
iLn:3 ^ log3 (α n) <= α n < 3 ^ (log3 (α n)).+1
81f
  rewrite gtn_log3  leq_log3 //.
7af
0 < α n
824
  by apply: alpha_gt0.
826
81f
by apply: sum_alpha_eq.
Qed.

Lemma S1_bigmin n : 
  S1 n.+1 = \min_(i <= n) ((S1 i).*2 + (3 ^ (n.+1 - i)).-1./2).
7af
S1 n.+1 =
\min_(i <= n) ((S1 i).*2 + ((3 ^ (n.+1 - i)).-1)./2)
Proof.
830
apply/eqP; rewrite eqn_leq; apply/andP; split; last first.
7af
\min_(i <= n) ((S1 i).*2 + ((3 ^ (n.+1 - i)).-1)./2) <=
S1 n.+1
7af
S1 n.+1 <=
\min_(i <= n) ((S1 i).*2 + ((3 ^ (n.+1 - i)).-1)./2)
  rewrite S1_eq // -{2}(subKn (leq_log3_alpha n)).
7af
\min_(i <= n) ((S1 i).*2 + ((3 ^ (n.+1 - i)).-1)./2) <=
(S1 (n.+1 - (log3 (α n.+1.-1)).+1)).*2 +
((3 ^ (n.+1 - (n.+1 - (log3 (α n)).+1))).-1)./2
838
  apply: bigmin_inf (leqnn _) => //.
7af
n.+1 - (log3 (α n.+1.-1)).+1 <= n
838
  by rewrite leq_subLR addSnnS leq_addl.
7af
83a
apply/bigmin_leqP => i iLn.
7bb
S1 n.+1 <= (S1 i).*2 + ((3 ^ (n.+1 - i)).-1)./2
rewrite -{1}(subKn (_ : i <= n.+1)); last by apply: ltnW.
7bb
S1 n.+1 <=
(S1 (n.+1 - (n.+1 - i))).*2 + ((3 ^ (n.+1 - i)).-1)./2
by apply/S1_leq/leq_subr.
Qed.

Lemma delta_S1 n : delta S1 n = α n.
7af
delta S1 n = α n
Proof.
84f by rewrite /S1 /delta big_ord_recr /= addnC addnK. Qed. 

Definition dsum_alphaL l :=
 conv (fun i => (S1 i).*2) (fun i => l * (3 ^ i).-1./2).

Notation " 'S_[' l ']' " := (dsum_alphaL l) 
 (format "S_[ l ]").

Definition alphaL l n := delta S_[l] n.

Notation " 'α_[' l ']' " := (alphaL l) 
 (format "α_[ l ]").

Lemma leq_bigmin f g n :
 (forall i, i <= n -> f i <= g i) ->
 \min_(i <= n) f i <= \min_(i <= n) g i.
f, g:nat -> nat
19
(forall i : nat, i <= n -> f i <= g i) ->
\min_(i <= n) f i <= \min_(i <= n) g i
Proof.
854
elim: n => /= [->//|n IH H].
85719
IH:(forall i : nat, i <= n -> f i <= g i) ->
\min_(i <= n) f i <= \min_(i <= n) g i
H:forall i : nat, i <= n.+1 -> f i <= g i
minn (f n.+1) (\min_(i <= n) f i) <=
minn (g n.+1) (\min_(i <= n) g i)
rewrite leq_min !geq_min H //= orbC IH // => i iLn.
8571985e85f373c1
f i <= g i
by rewrite H // (leq_trans iLn).
Qed.

Lemma increasing_dsum_alphaL_l n : increasing (fun l => S_[l] n).
7af
increasing (dsum_alphaL^~ n)
Proof.
867
move=> l; rewrite /increasing /dsum_alphaL /conv.
n, l:nat
\min_(i <= n) ((S1 i).*2 + l * ((3 ^ (n - i)).-1)./2) <=
\min_(i <= n) ((S1 i).*2 +
               l.+1 * ((3 ^ (n - i)).-1)./2)
apply: leq_bigmin => i _.
n, l, i:nat
(S1 i).*2 + l * ((3 ^ (n - i)).-1)./2 <=
(S1 i).*2 + l.+1 * ((3 ^ (n - i)).-1)./2
by rewrite leq_add2l leq_mul2r leqnSn orbT.
Qed.

Lemma concave_dsum_alphaL_l n : concave (fun l => S_[l] n).
7af
concave (dsum_alphaL^~ n)
Proof.
878
apply: concaveE (increasing_dsum_alphaL_l _) _ => i.
7b5
S_[i] n + S_[i.+2] n <= (S_[i.+1] n).*2
rewrite {3}/dsum_alphaL /conv.
7b5
S_[i] n + S_[i.+2] n <=
(\min_(i0 <= n) ((S1 i0).*2 +
                 i.+1 * ((3 ^ (n - i0)).-1)./2)).*2
pose f i x := (S1 x).*2 + i * ((3 ^ (n - x)).-1)./2.
43
f:=fun i x : nat =>
(S1 x).*2 + i * ((3 ^ (n - x)).-1)./2:nat -> nat -> nat
883
case: (eq_bigmin (f i.+1) n) => j ->.
43888
j:'I_n.+1
S_[i] n + S_[i.+2] n <= (f i.+1 j).*2
have -> : (f i.+1 j).*2 = f i j + f (i.+2) j.
88c
(f i.+1 j).*2 = f i j + f i.+2 j
88c
S_[i] n + S_[i.+2] n <= f i j + f i.+2 j
  rewrite /f; set x := (S1 _).*2; set y := _./2.
4388888d
x:=(S1 j).*2:nat
y:=((3 ^ (n - j)).-1)./2:nat
(x + i.+1 * y).*2 = x + i * y + (x + i.+2 * y)
893
  rewrite addnCA 2![in RHS]addnA addnn -[in RHS]addnA -mulnDl.
899
(x + i.+1 * y).*2 = x.*2 + (i + i.+2) * y
893
  by rewrite -addSnnS addnn -doubleMl -doubleD.
88c
895
apply: leq_add.
88c
S_[i] n <= f i j
88c
S_[i.+2] n <= f i.+2 j
  by apply: bigmin_inf (leqnn _); rewrite -ltnS.
88c
8aa
by apply: bigmin_inf (leqnn _); rewrite -ltnS.
Qed.

Lemma lim_dsum_alphaL_l l n : (S1 n).*2 <= l -> S_[l] n = (S1 n).*2.
l, n:nat
(S1 n).*2 <= l -> S_[l] n = (S1 n).*2
Proof.
8af
move=> S1Ll; apply/eqP.
8b2
S1Ll:(S1 n).*2 <= l
S_[l] n == (S1 n).*2
rewrite /dsum_alphaL /conv eqn_leq; apply/andP; split.
8b8
\min_(i <= n) ((S1 i).*2 + l * ((3 ^ (n - i)).-1)./2) <=
(S1 n).*2
8b8
(S1 n).*2 <=
\min_(i <= n) ((S1 i).*2 + l * ((3 ^ (n - i)).-1)./2)
  apply: bigmin_inf (_ : _ n <= _) => //.
8b8
(S1 n).*2 + l * ((3 ^ (n - n)).-1)./2 <= (S1 n).*2
8bf
  by rewrite subnn muln0 addn0.
8b8
8c1
apply/bigmin_leqP => i.
8b28b937
i <= n ->
(S1 n).*2 <= (S1 i).*2 + l * ((3 ^ (n - i)).-1)./2
case: ltngtP => // [iLn _|-> _]; last apply: leq_addr.
8b28b937
iLn:i < n
(S1 n).*2 <= (S1 i).*2 + l * ((3 ^ (n - i)).-1)./2
apply: leq_trans S1Ll _.
l, n, i:nat
8d2
l <= (S1 i).*2 + l * ((3 ^ (n - i)).-1)./2
apply: leq_trans (leq_addl _ _).
8d7
l <= l * ((3 ^ (n - i)).-1)./2
rewrite -{1}[l]muln1 leq_mul2l (half_leq (_ : 2 <= _)) ?orbT //.
8d7
1 < (3 ^ (n - i)).-1
by rewrite -ltnS prednK ?expn_gt0 // (@leq_exp2l _ 1) // subn_gt0.
Qed.

Lemma delta_2S1 i : delta (fun i : nat => (S1 i).*2) i = (α i).*2.
37
delta (fun i : nat => (S1 i).*2) i = (α i).*2
Proof.
8e3 by rewrite /delta -doubleB [_ - _]delta_S1. Qed.

Lemma convex_2S1 : convex (fun i : nat => (S1 i).*2).
convex (fun i : nat => (S1 i).*2)
Proof.
8e9
split => [] i.
8e5
(S1 i).*2 <= (S1 i.+1).*2
8e5
delta (fun i : nat => (S1 i).*2) i <=
delta (fun i : nat => (S1 i).*2) i.+1
  by rewrite leq_double /dsum_alpha [X in _ <= X]big_ord_recr leq_addr.
8e5
8f3
by rewrite !delta_2S1 leq_double; apply/ltnW/alpha_ltn.
Qed.

Lemma delta_3l l i : delta (fun i : nat => l * ((3 ^ i).-1)./2) i = l * 3 ^ i.
l, i:nat
delta (fun i : nat => l * ((3 ^ i).-1)./2) i =
l * 3 ^ i
Proof.
8f8
rewrite /delta -mulnBr -even_halfB //;
  try by rewrite -subn1 oddB ?expn_gt0 //= oddX orbT.
8fa
l * ((3 ^ i.+1).-1 - (3 ^ i).-1)./2 = l * 3 ^ i
rewrite -predn_sub -subnS prednK ?expn_gt0 //.
8fa
l * (3 ^ i.+1 - 3 ^ i)./2 = l * 3 ^ i
by rewrite expnS -[X in _ * ((_ - X))./2]mul1n -mulnBl mul2n doubleK.
Qed.

Lemma convex_3l l : convex (fun i : nat => l * ((3 ^ i).-1)./2).
l:nat
convex (fun i : nat => l * ((3 ^ i).-1)./2)
Proof.
907
split => [] i.
8fa
l * ((3 ^ i).-1)./2 <= l * ((3 ^ i.+1).-1)./2
8fa
delta (fun i : nat => l * ((3 ^ i).-1)./2) i <=
delta (fun i : nat => l * ((3 ^ i).-1)./2) i.+1
  rewrite leq_mul2l half_leq ?orbT //.
8fa
(3 ^ i).-1 <= (3 ^ i.+1).-1
911
  by apply: leq_pred2; rewrite leq_exp2l.
8fa
913
by rewrite !delta_3l leq_mul2l leq_exp2l // leqnSn orbT.
Qed.

Lemma convex_dsum_alphaL l : convex (S_[l]).
909
convex S_[l]
Proof.
91c
apply: convex_conv; first by apply: convex_2S1.
907
by apply: convex_3l.
Qed.

Lemma alphaLE l n : 
  α_[l] n = fmerge (fun i : nat => (α i).*2) (fun i : nat => l * 3 ^ i) n.
8b1
α_[l] n =
fmerge (fun i : nat => (α i).*2)
  (fun i : nat => l * 3 ^ i) n
Proof.
922
rewrite [LHS]delta_conv; last by apply: convex_3l.
8b1
fmerge (delta (fun i : nat => (S1 i).*2))
  (delta (fun i : nat => l * ((3 ^ i).-1)./2)) n =
fmerge (fun i : nat => (α i).*2)
  (fun i : nat => l * 3 ^ i) n
8b1
8eb
  apply: fmerge_ext => i; first by rewrite delta_2S1.
8d8
8fc
92a
  by rewrite delta_3l.
8b1
8eb
by apply: convex_2S1.
Qed.

Lemma increasing_alphaL l : increasing α_[l].
909
increasing α_[l]
Proof.
934
apply: increasing_ext; first by move=> i; apply/sym_equal/alphaLE.
909
increasing
  (fmerge (fun i : nat => (α i).*2)
     (fun i : nat => l * 3 ^ i))
apply: increasing_fmerge.
909
increasing (fun i : nat => (α i).*2)
909
increasing (fun i : nat => l * 3 ^ i)
  by move=> n; rewrite leq_double; apply/ltnW/alpha_mono.
909
942
by move=> n; rewrite leq_mul2l leq_exp2l ?leqnSn ?orbT.
Qed.

Lemma increasing_alphaL_l n : increasing (fun l => α_[l] n).
7af
increasing (alphaL^~ n)
Proof.
947
move=> l; rewrite !alphaLE !fmergeE //; last 4 first.
86e
93f
86e
increasing (fun i : nat => l.+1 * 3 ^ i)
86e
93f
86e
942
86e
\max_(i < n.+1) minn (α i).*2 (l * 3 ^ (n - i)) <=
\max_(i < n.+1) minn (α i).*2 (l.+1 * 3 ^ (n - i))
-
94c by move=> k; rewrite leq_double; apply/ltnW/alpha_mono.
86e
950
951952953
-
957 by move=> k; rewrite leq_mul2l leq_exp2l ?leqnSn ?orbT.
94d
952953
-
95c by move=> k; rewrite leq_double; apply/ltnW/alpha_mono.
86e
942
953
-
960 by move=> k; rewrite leq_mul2l leq_exp2l ?leqnSn ?orbT.
86e
954
apply/bigmax_leqP => i _.
86f
i:ordinal_finType n.+1
minn (α i).*2 (l * 3 ^ (n - i)) <=
\max_(i < n.+1) minn (α i).*2 (l.+1 * 3 ^ (n - i))
apply: leq_trans (_ : minn (α i).*2 (l.+1 * 3 ^ (n - i)) <= _).
96a
minn (α i).*2 (l * 3 ^ (n - i)) <=
minn (α i).*2 (l.+1 * 3 ^ (n - i))
96a
minn (α i).*2 (l.+1 * 3 ^ (n - i)) <=
\max_(i < n.+1) minn (α i).*2 (l.+1 * 3 ^ (n - i))
  by rewrite leq_min !geq_min leqnn /= leq_mul2r leqnSn !orbT.
96a
973
by apply: leq_bigmax.
Qed.

Lemma submodular_dsum_alphaL l n :
  S_[l] n.+1 + S_[l.+1] n <= S_[l] n + S_[l.+1] n.+1.
8b1
S_[l] n.+1 + S_[l.+1] n <= S_[l] n + S_[l.+1] n.+1
Proof.
978
rewrite -leq_subLR -addnBAC; last first.
8b1
S_[l] n <= S_[l] n.+1
8b1
S_[l] n.+1 - S_[l] n + S_[l.+1] n <= S_[l.+1] n.+1
  by have [daI _] := convex_dsum_alphaL l.
8b1
982
rewrite -[_ - _]/(α_[l] _) addnC -leq_subRL; last first.
8b1
S_[l.+1] n <= S_[l.+1] n.+1
8b1
α_[l] n <= S_[l.+1] n.+1 - S_[l.+1] n
  by have [daI _] := convex_dsum_alphaL l.+1.
8b1
98c
 rewrite -[_ - _]/(α_[l.+1] _).
8b1
α_[l] n <= α_[l.+1] n
by apply: increasing_alphaL_l.
Qed.

Lemma alphaL_0 l : α_[l] 0 = minn 2 l.
909
α_[l] 0 = minn 2 l
Proof.
995
rewrite /alphaL /delta /dsum_alphaL /conv /= dsum_alpha_1 dsum_alpha_0.
909
minn (1.*2 + l * 0) (0.*2 + l * 1) - (0.*2 + l * 0) =
minn 2 l
by rewrite muln0 addn0 add0n subn0 muln1.
Qed.

Lemma S0E n : S_[0] n = 0.
7af
S_[0] n = 0
Proof.
99e
rewrite /dsum_alphaL /conv.
7af
\min_(i <= n) ((S1 i).*2 + 0 * ((3 ^ (n - i)).-1)./2) =
0
elim: n => /= [|n ->]; first by rewrite dsum_alpha_0.
7af
minn ((S1 n.+1).*2 + 0 * ((3 ^ (n.+1 - n.+1)).-1)./2)
  0 = 0
by rewrite minn0.
Qed.

Lemma S1E : S_[1] =1 S1.
S_[1] =1 S1
Proof.
9ab
case => [|i].
S_[1] 0 = S1 0
8e5
S_[1] i.+1 = S1 i.+1
  by rewrite /dsum_alphaL /conv /= dsum_alpha_0.
8e5
9b5
rewrite S1_bigmin /dsum_alphaL /conv /= subnn addn0 -S1_bigmin.
8e5
minn (S1 i.+1).*2
  (\min_(i0 <= i) ((S1 i0).*2 +
                   1 * ((3 ^ (i.+1 - i0)).-1)./2)) =
S1 i.+1
rewrite (_ : \min_(_ <= _) _ = S1 i.+1).
8e5
minn (S1 i.+1).*2 (S1 i.+1) = S1 i.+1
8e5
\min_(x <= i) ((S1 x).*2 +
               1 * ((3 ^ (i.+1 - x)).-1)./2) = S1 i.+1
  by rewrite (minn_idPr _) // -addnn leq_addr.
8e5
9c3
by rewrite S1_bigmin; apply: bigmin_ext => i1 i1H; rewrite mul1n.
Qed.



Lemma bound_dsum_alphaL l n : S_[l] n <= (S_[1] n).*2.
8b1
S_[l] n <= (S_[1] n).*2
Proof.
9c8
rewrite S1E.
8b1
S_[l] n <= (S1 n).*2
have [SLl|lLS] := leqP (S1 n).*2 l; first by rewrite lim_dsum_alphaL_l.
8b2
lLS:l < (S1 n).*2
9cf
rewrite -(lim_dsum_alphaL_l (leqnn _)).
9d3
S_[l] n <= S_[(S1 n).*2] n
have [/increasingE H _] := concave_dsum_alphaL_l n.
8b29d4
H:forall n0 n1 : nat,
n0 <= n1 -> S_[n0] n <= S_[n1] n
9d8
by apply/H/ltnW.
Qed.

Lemma alphaL1E k : α_[1] k = α k.
528
α_[1] k = α k
Proof.
9df by rewrite /alphaL /delta !S1E -delta_S1. Qed.


Lemma bound_alphaL l n : α_[l] n <= (α_[1] n).*2.
8b1
α_[l] n <= (α_[1] n).*2
Proof.
9e5
rewrite alphaL1E.
8b1
α_[l] n <= (α n).*2
have [SLl|lLS] := leqP (S1 n.+1).*2 l.
8b2
SLl:(S1 n.+1).*2 <= l
9ec
8b2
lLS:l < (S1 n.+1).*2
9ec
 rewrite /alphaL /delta !lim_dsum_alphaL_l //.
9f0
(S1 n.+1).*2 - (S1 n).*2 <= (α n).*2
9f0
(S1 n).*2 <= l
9f3
   by rewrite -delta_S1 doubleB.
9f0
9fc
9f2
 by apply: leq_trans SLl; case: convex_2S1.
9f4
9ec
rewrite -delta_S1 /delta doubleB.
9f4
α_[l] n <= (S1 n.+1).*2 - (S1 n).*2
rewrite -(lim_dsum_alphaL_l (leqnn _)).
9f4
α_[l] n <= S_[(S1 n.+1).*2] n.+1 - (S1 n).*2
rewrite -[(S1 n).*2](@lim_dsum_alphaL_l (S1 n.+1).*2).
9f4
α_[l] n <= S_[(S1 n.+1).*2] n.+1 - S_[(S1 n.+1).*2] n
9f4
(S1 n).*2 <= (S1 n.+1).*2
  rewrite -[_ - _]/(α_[_] _).
9f4
α_[l] n <= α_[(S1 n.+1).*2] n
a0f
  by apply: increasingE (increasing_alphaL_l n) _; apply: ltnW.
9f4
a11
by case: convex_2S1.
Qed.

Lemma iotaS m n : iota m n.+1 = m :: iota m.+1 n.
17c
iota m n.+1 = m :: iota m.+1 n
Proof.
a1a by []. Qed.

Lemma count_cons (T : Type) a b (l : seq T) : count a (b :: l) = a b + count a l.
T:Type
a:pred T
b:T
12
count a (b :: l) = a b + count a l
Proof.
a20 by []. Qed.


Lemma increasing_alpha : increasing α.
increasing α
Proof.
a29 by move=> n; apply/ltnW/alpha_mono. Qed.

(* THis is 3.3 *)
Lemma alpha_min_exp3 m k : α m + minn (3 ^ k) (α m) <= α (m + k.+1).
m, k:nat
α m + minn (3 ^ k) (α m) <= α (m + k.+1)
Proof.
a2e
case: (leqP (α m).*2 (α (m + k.+1))) => [/(leq_trans _)-> //|amkLam].
a30
α m + minn (3 ^ k) (α m) <= (α m).*2
a31
amkLam:α (m + k.+1) < (α m).*2
a32
  by rewrite -addnn leq_add2l geq_minr.
a3a
a32
apply: leq_trans (leq_add (leqnn _) (geq_minl _ _)) _.
a3a
α m + 3 ^ k <= α (m + k.+1)
move: m amkLam => n; rewrite [_ + 3 ^ _]addnC.
521
α (n + k.+1) < (α n).*2 -> 3 ^ k + α n <= α (n + k.+1)  
set m := n + k.+1.
521
m:=n + k.+1:nat
α m < (α n).*2 -> 3 ^ k + α n <= α m
have : k + n < m by rewrite /m addnS addnC.
a4b
k + n < m -> α m < (α n).*2 -> 3 ^ k + α n <= α m
move: m => m.
k, n, m:nat
a51
elim: k m n => [m n | k IH m n nkLm aL2a].
a1c
0 + n < m -> α m < (α n).*2 -> 3 ^ 0 + α n <= α m
528
IH:forall m n : nat,
k + n < m -> α m < (α n).*2 -> 3 ^ k + α n <= α m
17c
nkLm:k.+1 + n < m
aL2a:α m < (α n).*2
3 ^ k.+1 + α n <= α m
  by rewrite add0n add1n => nLm _; apply: alpha_mono.
a5d
a61
pose l := [seq (α i) | i <- iota n (m - n).+1 & 3 %| (α i)].
528a5e17ca5fa60
l:=[seq α i | i <- iota n (m - n).+1 & 3 %| α i]:seq nat
a61
have Il i : i \in l -> exists j, i = 3 * α j.
528a5e17ca5fa60a6930
i \in l -> exists j : nat, i = 3 * α j
528a5e17ca5fa60a69
Il:forall i : nat_eqType,
i \in l -> exists j : nat, i = 3 * α j
a61
  case/mapP => j; rewrite mem_filter => /andP[ajD3 _] ->.
528a5e17ca5fa60a69
i, j:nat_eqType
ajD3:3 %| α j
exists j0 : nat, α j = 3 * α j0
a6f
  have [[i1 [|j1]] /= ajE]: isAB 2 3 (α j) by apply: isAB_alpha.
528a5e17ca5fa60a69a77a78
i1:nat
ajE:α j = 2 ^ i1 * 3 ^ 0
a79
528a5e17ca5fa60a69a77a78
i1, j1:nat
ajE:α j = 2 ^ i1 * 3 ^ j1.+1
a79
a70
    by move: ajD3; rewrite ajE muln1 Euclid_dvdX //.
a82
a79
a6f
  have [k1 ak1E] : {k : nat | α k = 2 ^ i1 * 3 ^ j1} by apply: alpha_surjective.
528a5e17ca5fa60a69a77a78a83a84
k1:nat
ak1E:α k1 = 2 ^ i1 * 3 ^ j1
a79
a6f
  by exists k1; rewrite ak1E ajE expnS mulnCA.
a71
a61
have nLm : n <= m by rewrite (leq_trans _ nkLm) // -addSn leq_addl.
528a5e17ca5fa60a69a72
nLm:n <= m
a61
have iS : k.+3 <= size (iota n (m - n).+1).
a94
k.+2 < size (iota n (m - n).+1)
528a5e17ca5fa60a69a72a95
iS:k.+2 < size (iota n (m - n).+1)
a61
  by rewrite size_iota ltnS leq_subRL // addnC addSn.
a9c
a61
have kLsl : k.+2 <= size l.
a9c
k.+1 < size l
528a5e17ca5fa60a69a72a95a9d
kLsl:k.+1 < size l
a61
  rewrite size_map size_filter -ltnS -[X in _ < X]add1n.
a9c
k.+2 <
1 +
count (fun i : nat => 3 %| α i) (iota n (m - n).+1)
aa5
  move: iS; rewrite -(count_predC (fun i => 3 %| (α i))) -/l => iS.
528a5e17ca5fa60a69a72a95
iS:k.+2 <
count (fun i : nat => 3 %| α i)
  (iota n (m - n).+1) +
count (predC (fun i : nat => 3 %| α i))
  (iota n (m - n).+1)
aac
aa5
  apply: leq_trans iS _; rewrite addnC leq_add2r.
a94
count (predC (fun i : nat => 3 %| α i))
  (iota n (m - n).+1) <= 1
aa5
  move: aL2a; rewrite -{1}(subnK nLm) addnC.
528a5e17ca5fa69a72a95
α (n + (m - n)) < (α n).*2 ->
count (predC (fun i : nat => 3 %| α i))
  (iota n (m - n).+1) <= 1
aa5
  move: (m - n) => u.
528a5e17ca5fa69a72a95
u:nat
α (n + u) < (α n).*2 ->
count (predC (fun i : nat => 3 %| α i)) (iota n u.+1) <=
1
aa5
  elim: u {k IH Il l nLm nkLm}n => [n _ /=|k IH n H]; first by case: negb.
a31
IH:forall n : nat,
α (n + k) < (α n).*2 ->
count (predC (fun i : nat => 3 %| α i))
  (iota n k.+1) <= 1
19
H:α (n + k.+1) < (α n).*2
count (predC (fun i : nat => 3 %| α i)) (iota n k.+2) <=
1
aa5
  have /IH : α (n.+1 + k) < (α n.+1).*2.
ac4
α (n.+1 + k) < (α n.+1).*2
ac4
count (predC (fun i : nat => 3 %| α i))
  (iota n.+1 k.+1) <= 1 ->
count (predC (fun i : nat => 3 %| α i)) (iota n k.+2) <=
1
aa6
    by rewrite addSnnS (leq_trans H) // leq_double ltnW // alpha_mono.
ac4
ace
aa5
  rewrite (iotaS _ _.+1) count_cons.
ac4
count (predC (fun i : nat => 3 %| α i))
  (iota n.+1 k.+1) <= 1 ->
predC (fun i : nat => 3 %| α i) n +
count (predC (fun i : nat => 3 %| α i))
  (iota n.+1 k.+1) <= 1
aa5
  case: ltngtP => // [|H1 _].
ac4
count (predC (fun i : nat => 3 %| α i))
  (iota n.+1 k.+1) < 1 ->
true ->
predC (fun i0 : nat => 3 %| α i0) n +
count (predC (fun i0 : nat => 3 %| α i0))
  (iota n.+1 k.+1) <= 1
a31ac519ac6
H1:count (predC (fun i : nat => 3 %| α i))
  (iota n.+1 k.+1) = 1
predC (fun i : nat => 3 %| α i) n +
count (predC (fun i : nat => 3 %| α i))
  (iota n.+1 k.+1) <= 1
aa6
    by case: count => //=; case: (~~ _).
adc
ade
aa5
  have /hasP[i iH1 iH2] : has (predC (fun i => 3 %| α i)) (iota n.+1 k.+1).
adc
has (predC (fun i : nat => 3 %| α i)) (iota n.+1 k.+1)
a31ac519ac6add30
iH1:i \in iota n.+1 k.+1
iH2:predC (fun i : nat => 3 %| α i) i
ade
aa6
    by rewrite has_count H1.
ae8
ade
aa5
  move: iH1; rewrite mem_iota => /andP[nLi iLn].
a31ac519ac6add30aea
nLi:n < i
iLn:i < n.+1 + k.+1
ade
aa5
  rewrite H1; case: (boolP (predC _ _)) => //= iH3.
a31ac519ac6add30aeaaf2af3
iH3:~~ (3 %| α n)
1 + 1 <= 1
aa5
  have [[i1 [|j1]] /= aiE] : isAB 2 3 (α i) by apply: isAB_alpha.
a31ac519ac6add30aeaaf2af3af8a7e
aiE:α i = 2 ^ i1 * 3 ^ 0
af9
a31ac519ac6add30aeaaf2af3af8a83
aiE:α i = 2 ^ i1 * 3 ^ j1.+1
af9
aa6
    have [[i2 [|j2]] /= anE] : isAB 2 3 (α n) by apply: isAB_alpha.
a31ac519ac6add30aeaaf2af3af8a7eafe
i2:nat
anE:α n = 2 ^ i2 * 3 ^ 0
af9
a31ac519ac6add30aeaaf2af3af8a7eafe
i2, j2:nat
anE:α n = 2 ^ i2 * 3 ^ j2.+1
af9
b00aa6
      rewrite !muln1 in aiE anE.
a31ac519ac6add30aeaaf2af3af8
i1, i2:nat
aiE:α i = 2 ^ i1
anE:α n = 2 ^ i2
af9
b09
      have : α n < α i by apply: alpha_mono.
b11
α n < α i -> 1 + 1 <= 1
b09
      rewrite aiE anE ltn_exp2l // => i2Li1.
a31ac519ac6add30aeaaf2af3af8b12b13b14
i2Li1:i2 < i1
af9
b09
      have : (α i) < (α n).*2.
b1c
α i < (α n).*2
b1c
α i < (α n).*2 -> 1 + 1 <= 1
b0ab00aa6
        apply: leq_trans H; rewrite ltnS -addSnnS //.
a31ac519add30aeaaf2af3af8b12b13b14b1d
α i <= α (n.+1 + k)
b22
        move: iLn;rewrite addnS ltnS; case: ltngtP => // [iLS _|<-//].
a31ac519add30aeaaf2af8b12b13b14b1d
iLS:i < n.+1 + k
b29
b22
        by apply/ltnW/alpha_mono.
b1c
b24
b09
      by rewrite aiE anE -mul2n -expnS ltn_exp2l // ltnS leqNgt i2Li1.
b0b
af9
aff
    by case/negP : iH3; rewrite anE expnS mulnCA dvdn_mulr.
b01
af9
aa5
  by case/negP : iH2; rewrite aiE expnS mulnCA dvdn_mulr.
aa7
a61
pose n1 := head 0 l.
528a5e17ca5fa60a69a72a95a9daa8
n1:=head 0 l:nat
a61
pose m1 := last 0 l.
528a5e17ca5fa60a69a72a95a9daa8b3f
m1:=last 0 l:nat
a61
have lS : sorted ltn l.
b43
sorted ltn l
528a5e17ca5fa60a69a72a95a9daa8b3fb44
lS:sorted ltn l
a61
  rewrite sorted_map.
b43
sorted (relpre [eta α] ltn)
  [seq i <- iota n (m - n).+1 | 3 %| α i]
b49
  apply: sorted_filter.
b43
transitive (relpre [eta α] ltn)
b43
sorted (relpre [eta α] ltn) (iota n (m - n).+1)
b4a
    by move=> a b c H1 H2; apply: ltn_trans H2.
b43
b57
b49
  move: (_ - _).+1 => u; elim: u (n) => //= k1 IH1 n0.
528a5e17ca5fa60a69a72a95a9daa8b3fb44a8c
IH1:forall n : nat,
sorted (relpre [eta α] ltn) (iota n k1)
n0:nat
path (relpre [eta α] ltn) n0 (iota n0.+1 k1)
b49
  by case: (k1) (IH1 n0.+1) => //= k2 -; rewrite alpha_mono.
b4b
a61
have uS : uniq l by move: lS; rewrite ltn_sorted_uniq_leq; case/andP.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4c
uS:uniq l
a61
have n1Il : n1 \in l.
b68
n1 \in l
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69
n1Il:n1 \in l
a61
  by rewrite /n1; case: (l) kLsl => [|a l1]; rewrite /= ?inE ?eqxx.
b70
a61
case: (Il _ n1Il) => n2 n2E.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71
n2:nat
n2E:n1 = 3 * α n2
a61
have m1Il : m1 \in l.
b78
m1 \in l
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7a
m1Il:m1 \in l
a61
  by rewrite /m1; case: (l) kLsl => [|a l1]; rewrite //= mem_last.
b81
a61
case: (Il _ m1Il) => m2 m2E.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82
m2:nat
m2E:m1 = 3 * α m2
a61
have n1Lm1 : n1 < m1.
b89
n1 < m1
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8b
n1Lm1:n1 < m1
a61
  rewrite /n1 /m1; case: (l) kLsl lS => [|a [|b l1 _]] //= /andP[].
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8b5
l1:seq nat
a < b -> path ltn b l1 -> a < last b l1
b90
  elim: l1 a b => //= c l1 IH1 a b aLb /andP[bLc pH].
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8bf8b98
IH1:forall a b : nat,
a < b -> path ltn b l1 -> a < last b l1
57
bLc:b < c
pH:path ltn c l1
a < last c l1
b90
  by apply: ltn_trans aLb (IH1 _ _ _ _).
b92
a61
have n2Lm2 : n2 < m2.
b92
n2 < m2
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93
n2Lm2:n2 < m2
a61
  move: n1Lm1; rewrite n2E m2E ltn_mul2l /=.
b89
α n2 < α m2 -> n2 < m2
ba9
  case: (ltngtP n2 m2) => // [m2Ln2|->]; last by rewrite ltnn.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8b
m2Ln2:m2 < n2
α n2 < α m2 -> false
ba9
  by rewrite ltnNge ltnW // alpha_mono.
bab
a61
pose l1 := [seq 3 * α i | i <- iota n2 (m2 - n2).+1].
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bac
l1:=[seq 3 * α i | i <- iota n2 (m2 - n2).+1]:seq nat
a61
have l1size : size l1 = (m2 - n2).+1 by rewrite size_map size_iota.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbe
l1size:size l1 = (m2 - n2).+1
a61
have H : {subset l <= l1}.
bc2
{subset l <= l1}
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc3
H:{subset l <= l1}
a61
  move=> i iIl; case: (Il _ iIl) => j jE.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc330
iIl:i \in l
j:nat
jE:i = 3 * α j
i \in l1
bc8
  apply/mapP; exists j; rewrite // mem_iota addnS addnC subnK //; last first.
bcf
n2 <= m2
bcf
n2 <= j < m2.+1
bc9
    by rewrite ltnW.
bcf
bda
bc8
  rewrite ltnS; apply/andP; split.
bcf
n2 <= j
bcf
j <= m2
bc9
    have: n1 <= i.
bcf
n1 <= i
bcf
n1 <= i -> n2 <= j
be3bc9
      rewrite /n1; case: (l) kLsl iIl lS => //= a l2 _.
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8bb93bacbbebc330bd1bd2
a:nat
l2:seq nat
i \in a :: l2 -> path ltn a l2 -> a <= i
be9
      rewrite inE => /orP[/eqP->//|].
bef
i \in l2 -> path ltn a l2 -> a <= i
be9
      elim: l2 a => //= b l2 IH1 a.
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8bb93bacbbebc330bd1bd2
b:nat
bf1
IH1:forall a : nat,
i \in l2 -> path ltn a l2 -> a <= i
bf0
i \in b :: l2 -> (a < b) && path ltn b l2 -> a <= i
be9
      rewrite inE => /orP[/eqP->//|bIl2] /andP[aLb pH]; first by apply: ltnW.
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8bb93bacbbebc330bd1bd2bfbbf1bfcbf0
bIl2:i \in l2
7
pH:path ltn b l2
a <= i
be9
      apply: leq_trans (ltnW aLb) _.
c01
b <= i
be9
      by apply: IH1.
bcf
beb
be2
    rewrite n2E jE leq_mul2l /=; case: (ltngtP n2 j) => // jLn2.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc330bd0bd1bd2
jLn2:j < n2
α n2 <= α j -> false
be2
    by rewrite leqNgt alpha_mono.
bcf
be4
bc8
  have: i <= m1.
bcf
i <= m1
bcf
i <= m1 -> j <= m2
bc9
    rewrite /m1; case: (l) kLsl iIl lS => //= a l2 _.
bef
i \in a :: l2 -> path ltn a l2 -> i <= last a l2
c19
    elim: l2 a (i) => /= [a i1|b l2 IH1 a i1]; first by rewrite inE => /eqP->.
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8bb93bacbbebc330bd1bd2bfbbf1
IH1:forall a i : nat,
i \in a :: l2 -> path ltn a l2 -> i <= last a l2
a, i1:nat
i1 \in [:: a, b & l2] ->
(a < b) && path ltn b l2 -> i1 <= last b l2
c19
    rewrite inE => /orP[/eqP->//|bIl2] /andP[aLb pH].
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8bb93bacbbebc330bd1bd2bfbbf1c24c257c03
a <= last b l2
528a5e17ca5fa60a69a72a95a9db3fb44b69b71b79b7ab82b8ab8bb93bacbbebc330bd1bd2bfbbf1c24c25
bIl2:i1 \in b :: l2
7c03
i1 <= last b l2
c1abc9
      apply: leq_trans (ltnW aLb) (IH1 _ _ _ _) => //.
c2a
b \in b :: l2
c2c
      by rewrite inE eqxx.
c2e
c30
c19
    by apply: IH1.
bcf
c1b
bc8
  rewrite m2E jE leq_mul2l /=; case: (ltngtP m2 j) => // jLn2.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc330bd0bd1bd2
jLn2:m2 < j
α j <= α m2 -> false
bc8
  by rewrite leqNgt alpha_mono.
bca
a61
have kn2Lm2 : k + n2 < m2.
bca
k + n2 < m2
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc3bcb
kn2Lm2:k + n2 < m2
a61
  rewrite -addSn addnC -leq_subRL; last by apply: ltnW.
bca
k < m2 - n2
c48
  by rewrite -ltnS -l1size (leq_trans kLsl) // uniq_leq_size.
c4a
a61
have anLan2 : α n <= 3 * α n2.
c4a
α n <= 3 * α n2
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc3bcbc4b
anLan2:α n <= 3 * α n2
a61
  rewrite -n2E.
c4a
α n <= n1
c57
  case/mapP : n1Il => i1.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b79b7ab82b8ab8bb93bacbbebc3bcbc4b58
i1 \in [seq i <- iota n (m - n).+1 | 3 %| α i] ->
n1 = α i1 -> α n <= n1
c57
  rewrite mem_filter mem_iota => /andP[_ /andP[nLi1 _] ->].
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b79b7ab82b8ab8bb93bacbbebc3bcbc4b58
nLi1:n <= i1
α n <= α i1
c57
  by apply: (increasingE increasing_alpha).
c59
a61
have am2Lam : 3 * α m2 <= α m.
c59
3 * α m2 <= α m
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc3bcbc4bc5a
am2Lam:3 * α m2 <= α m
a61
  rewrite -m2E.
c59
m1 <= α m
c71
  case/mapP : m1Il => i1.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab8ab8bb93bacbbebc3bcbc4bc5a58
i1 \in [seq i <- iota n (m - n).+1 | 3 %| α i] ->
m1 = α i1 -> m1 <= α m
c71
  rewrite mem_filter mem_iota => /andP[_ /andP[_ i1Lm] ->].
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab8ab8bb93bacbbebc3bcbc4bc5a58
i1Lm:i1 < n + (m - n).+1
α i1 <= α m
c71
  rewrite addnS ltnS addnC subnK // in i1Lm.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab8ab8bb93bacbbebc3bcbc4bc5a58
i1Lm:i1 <= m
c83
c71
  by apply: (increasingE increasing_alpha).
c73
a61
have am2Lan2 : α m2 < (α n2).*2.
c73
α m2 < (α n2).*2
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc3bcbc4bc5ac74
am2Lan2:α m2 < (α n2).*2
a61
  rewrite -[_ < _]andTb -(ltn_mul2l 3) -doubleMr.
c73
3 * α m2 < (3 * α n2).*2
c90
  apply: leq_ltn_trans am2Lam _.
c59
α m < (3 * α n2).*2
c90
  apply: leq_trans aL2a _.
528a5e17ca5fa69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc3bcbc4bc5a
(α n).*2 <= (3 * α n2).*2
c90
  by rewrite leq_double.
c92
a61
apply: leq_trans am2Lam.
528a5e17ca5fa60a69a72a95a9daa8b3fb44b4cb69b71b79b7ab82b8ab8bb93bacbbebc3bcbc4bc5ac93
3 ^ k.+1 + α n <= 3 * α m2
apply: leq_trans (leq_add (leqnn _) anLan2) _.
ca7
3 ^ k.+1 + 3 * α n2 <= 3 * α m2
rewrite expnS -mulnDr leq_mul2l /=.
ca7
3 ^ k + α n2 <= α m2
by apply: IH kn2Lm2 am2Lan2.
Qed.

Lemma alpha_min_exp3_cor m k : 3 ^k <= α m -> α m + 3 ^ k <= α (m + k.+1).
a30
3 ^ k <= α m -> α m + 3 ^ k <= α (m + k.+1)
Proof.
cb2
move=> kLam.
a31
kLam:3 ^ k <= α m
a42
have := alpha_min_exp3 m k.
cb9
α m + minn (3 ^ k) (α m) <= α (m + k.+1) ->
α m + 3 ^ k <= α (m + k.+1)
by rewrite (minn_idPl _).
Qed.

Lemma eq_dsum_alphaL l n :
  {i : 'I_n.+1 | S_[l] n = (S1 i).*2 + l * ((3 ^ (n - i)).-1)./2}.
8b1
{i : 'I_n.+1
| S_[l] n = (S1 i).*2 + l * ((3 ^ (n - i)).-1)./2}
Proof.
cc0 by apply: eq_bigmin. Qed.

Lemma increasing_dsum_alpha : increasing S1.
increasing S1
Proof.
cc5
by move=> n; rewrite -leq_double; case: convex_2S1.
Qed.

Lemma even_expn3_pred n : ~~ odd (3 ^ n).-1.
7af
~~ odd (3 ^ n).-1
Proof.
cca
by rewrite -subn1 oddB ?expn_gt0 // oddX orbT.
Qed.

(* This is 3.4 *)
Lemma dsum_alphaL_alpha l n : 1 < l -> S_[l.+1] n.+1 <= S_[l] n + (α_[1] n).*2.
8b1
1 < l -> S_[l.+1] n.+1 <= S_[l] n + (α_[1] n).*2
Proof.
ccf
rewrite alphaL1E => l_gt1.
8b2
l_gt1:1 < l
S_[l.+1] n.+1 <= S_[l] n + (α n).*2
case: (eq_dsum_alphaL l n) => [] [/= m mLn] mH.
8b2cd7
m:nat
mLn:m < n.+1
mH:S_[l] n = (S1 m).*2 + l * ((3 ^ (n - m)).-1)./2
cd8
rewrite mH; rewrite ltnS in mLn.
8b2cd7cddcdf
mLn:m <= n
S_[l.+1] n.+1 <=
(S1 m).*2 + l * ((3 ^ (n - m)).-1)./2 + (α n).*2
apply: leq_trans (_ : (S1 m.+1).*2 + l.+1 * ((3 ^ (n - m)).-1)./2 <= _).
ce3
S_[l.+1] n.+1 <=
(S1 m.+1).*2 + l.+1 * ((3 ^ (n - m)).-1)./2
ce3
(S1 m.+1).*2 + l.+1 * ((3 ^ (n - m)).-1)./2 <=
(S1 m).*2 + l * ((3 ^ (n - m)).-1)./2 + (α n).*2
  by rewrite -subSS; apply: bigmin_inf (leqnn _).
ce3
cec
rewrite addnAC mulSn addnA leq_add2r.
ce3
(S1 m.+1).*2 + ((3 ^ (n - m)).-1)./2 <=
(S1 m).*2 + (α n).*2
rewrite -leq_subLR -addnBAC ?leq_double ?increasing_dsum_alpha //.
ce3
(S1 m.+1).*2 - (S1 m).*2 + ((3 ^ (n - m)).-1)./2 <=
(α n).*2
rewrite [_ - _]delta_2S1.
ce3
(α m).*2 + ((3 ^ (n - m)).-1)./2 <= (α n).*2
case: ltngtP mLn => // [mLn _ |-> _]; last by rewrite subnn addn0.
8b2cd7cddcdf
mLn:m < n
cfb
apply: leq_trans (_ : (α m).*2 + (3 ^ (n - m).-1).*2 <= _).
cff
(α m).*2 + ((3 ^ (n - m)).-1)./2 <=
(α m).*2 + (3 ^ (n - m).-1).*2
cff
(α m).*2 + (3 ^ (n - m).-1).*2 <= (α n).*2
  rewrite leq_add2l -leq_double.
cff
(((3 ^ (n - m)).-1)./2).*2 <= ((3 ^ (n - m).-1).*2).*2
d05
  apply: leq_trans (_ : (3 ^ (n - m)).-1 <= _).
cff
(((3 ^ (n - m)).-1)./2).*2 <= (3 ^ (n - m)).-1
cff
(3 ^ (n - m)).-1 <= ((3 ^ (n - m).-1).*2).*2
d06
    by rewrite -[X in _ <= X]odd_double_half leq_addl.
cff
d12
d05
  apply: leq_trans (ssrnat.leq_pred _) _.
cff
3 ^ (n - m) <= ((3 ^ (n - m).-1).*2).*2
d05
  by rewrite -[n -m]prednK ?subn_gt0 // expnSr -!muln2 -mulnA leq_mul.
cff
d07
rewrite -doubleD leq_double.
cff
α m + 3 ^ (n - m).-1 <= α n
have := @alpha_min_exp3_cor m (n - m).-1.
cff
(3 ^ (n - m).-1 <= α m ->
 α m + 3 ^ (n - m).-1 <= α (m + (n - m).-1.+1)) ->
α m + 3 ^ (n - m).-1 <= α n
rewrite prednK ?subn_gt0 // [_ + (_ - _)]addnC subnK; last by apply: ltnW.
cff
(3 ^ (n - m).-1 <= α m -> α m + 3 ^ (n - m).-1 <= α n) ->
α m + 3 ^ (n - m).-1 <= α n
apply.
cff
3 ^ (n - m).-1 <= α m
have : S_[l] n <= (S1 m.+1).*2 + l * (3 ^ (n - m.+1)).-1./2.
cff
S_[l] n <= (S1 m.+1).*2 + l * ((3 ^ (n - m.+1)).-1)./2
cff
S_[l] n <= (S1 m.+1).*2 + l * ((3 ^ (n - m.+1)).-1)./2 ->
3 ^ (n - m).-1 <= α m
  by apply: bigmin_inf mLn (leqnn _).
cff
d33
rewrite mH (_ : S1 m.+1 = S1 m + α m); last first.
cff
S1 m.+1 = S1 m + α m
cff
(S1 m).*2 + l * ((3 ^ (n - m)).-1)./2 <=
(S1 m + α m).*2 + l * ((3 ^ (n - m.+1)).-1)./2 ->
3 ^ (n - m).-1 <= α m
  by rewrite addnC -delta_S1 subnK // increasing_dsum_alpha.
cff
d3d
rewrite doubleD -!addnA leq_add2l.
cff
l * ((3 ^ (n - m)).-1)./2 <=
(α m).*2 + l * ((3 ^ (n - m.+1)).-1)./2 ->
3 ^ (n - m).-1 <= α m
rewrite addnC -leq_subLR -mulnBr -[_ <= α m]leq_double.
cff
l * (((3 ^ (n - m)).-1)./2 - ((3 ^ (n - m.+1)).-1)./2) <=
(α m).*2 -> (3 ^ (n - m).-1).*2 <= (α m).*2
rewrite -even_halfB ?even_expn3_pred //.
cff
l * ((3 ^ (n - m)).-1 - (3 ^ (n - m.+1)).-1)./2 <=
(α m).*2 -> (3 ^ (n - m).-1).*2 <= (α m).*2
have ->: (3 ^ (n - m)).-1 - (3 ^ (n - m.+1)).-1 = (3 ^ (n - m).-1).*2.
cff
(3 ^ (n - m)).-1 - (3 ^ (n - m.+1)).-1 =
(3 ^ (n - m).-1).*2
cff
l * ((3 ^ (n - m).-1).*2)./2 <= (α m).*2 ->
(3 ^ (n - m).-1).*2 <= (α m).*2
  rewrite subnS -{1}predn_sub -subnS prednK ?expn_gt0 //.
cff
3 ^ (n - m) - 3 ^ (n - m).-1 = (3 ^ (n - m).-1).*2
d51
  rewrite -{1}[(n - m)]prednK ?subn_gt0 // expnS.
cff
3 * 3 ^ (n - m).-1 - 3 ^ (n - m).-1 =
(3 ^ (n - m).-1).*2
d51
  by rewrite -mul2n -{4}[2]/(3 - 1) mulnBl mul1n.
cff
d53
by move=> /(leq_trans _)-> //; rewrite doubleK -mul2n leq_mul2r l_gt1 orbT.
Qed.

Lemma dsum_alphal_min_3  l n :
  S_[l] n.+1 = minn (S1 n.+1).*2 (S_[3 * l] n + l).
8b1
S_[l] n.+1 = minn (S1 n.+1).*2 (S_[3 * l] n + l)
Proof.
d60
rewrite {1}/dsum_alphaL /conv /= subnn muln0 addn0.
8b1
minn (S1 n.+1).*2
  (\min_(i <= n) ((S1 i).*2 +
                  l * ((3 ^ (n.+1 - i)).-1)./2)) =
minn (S1 n.+1).*2 (S_[3 * l] n + l)
congr (minn _ _).
8b1
\min_(i <= n) ((S1 i).*2 +
               l * ((3 ^ (n.+1 - i)).-1)./2) =
S_[3 * l] n + l
rewrite /dsum_alphaL /conv -bigmin_constD.
8b1
\min_(i <= n) ((S1 i).*2 +
               l * ((3 ^ (n.+1 - i)).-1)./2) =
\min_(i <= n) ((S1 i).*2 +
               3 * l * ((3 ^ (n - i)).-1)./2 + l)
apply: bigmin_ext => i iH; rewrite -addnA; congr (_ + _).
8d8
iH:i <= n
l * ((3 ^ (n.+1 - i)).-1)./2 =
3 * l * ((3 ^ (n - i)).-1)./2 + l
rewrite -mulnAC -{3}[l]mul1n -mulnDl mulnC; congr (_ * _).
d73
((3 ^ (n.+1 - i)).-1)./2 =
3 * ((3 ^ (n - i)).-1)./2 + 1
rewrite -even_halfMl ?even_expn3_pred // -{4}[1]/(2./2).
d73
((3 ^ (n.+1 - i)).-1)./2 =
(3 * (3 ^ (n - i)).-1)./2 + 2./2
rewrite -even_halfD ?oddM ?even_expn3_pred //; congr (_./2).
d73
(3 ^ (n.+1 - i)).-1 = 3 * (3 ^ (n - i)).-1 + 2
rewrite subSn // expnS -!subn1 mulnBr muln1 addn2 -!subSn ?subSS //.
d73
2 < (3 * 3 ^ (n - i)).+1
d73
2 < 3 * 3 ^ (n - i)
  by rewrite ltnS -expnS (ltn_exp2l 0).
d73
d88
by rewrite -expnS (leq_exp2l 1).
Qed.


(* This is first part of 3.5 *)
Lemma dsum_alpha3_S n : S_[1] n.+1 = (S_[3] n).+1.
7af
S_[1] n.+1 = (S_[3] n).+1
Proof.
d8d
rewrite S1E.
7af
S1 n.+1 = (S_[3] n).+1
have := dsum_alphal_min_3 1 n.
7af
S_[1] n.+1 = minn (S1 n.+1).*2 (S_[3 * 1] n + 1) ->
S1 n.+1 = (S_[3] n).+1
rewrite S1E addn1 /minn; case: leqP => // _ /eqP.
7af
S1 n.+1 == (S1 n.+1).*2 -> S1 n.+1 = (S_[3] n).+1
rewrite -addnn -{1}[S1 _]add0n eqn_add2r.
7af
0 == S1 n.+1 -> S1 n.+1 = (S_[3] n).+1
suff : 0 < S1 n.+1 by case: S1.
7af
0 < S1 n.+1
rewrite -dsum_alpha_1 increasingE //.
7af
cc7
by apply: increasing_dsum_alpha.
Qed.

Lemma alphaL_3E n : α_[3] n = α_[1] n.+1.
7af
α_[3] n = α_[1] n.+1
Proof.
da9
by rewrite /alphaL /delta -subSS -!dsum_alpha3_S.
Qed.

(* This is second part of 3.5 *)
Lemma dsum_alpha3l l n : S_[l] n.+1 <= S_[3 * l] n + l.
8b1
S_[l] n.+1 <= S_[3 * l] n + l
Proof.
dae
rewrite dsum_alphal_min_3.
8b1
minn (S1 n.+1).*2 (S_[3 * l] n + l) <= S_[3 * l] n + l
by apply: geq_minr.
Qed.

Lemma leq_dsum_alpha_2l_l l n : S_[l] n + S_[l] n.+1 <= (S_[l.*2] n).*2 + l.
8b1
S_[l] n + S_[l] n.+1 <= (S_[l.*2] n).*2 + l
Proof.
db7
have H := concaveEk (concave_dsum_alphaL_l n) (leq_addr l l).
8b2
H:S_[l + l - l] n + S_[l + l + l] n <=
(S_[l + l] n).*2
db9
rewrite addnK addnn -{1}mul2n -{3}[l]mul1n -mulnDl in H.
8b2
H:S_[l] n + S_[(2 + 1) * l] n <= (S_[l.*2] n).*2
db9
apply: leq_trans (leq_add H (leqnn _)).
dc3
S_[l] n + S_[l] n.+1 <=
S_[l] n + S_[(2 + 1) * l] n + l
by rewrite -addnA leq_add2l dsum_alpha3l.
Qed.

Lemma leq_dsum_alpha_2l_1 n : S_[1] n + S_[1] n.+1 <= (S_[2] n).*2.+1.
7af
S_[1] n + S_[1] n.+1 <= (S_[2] n).*2.+1
Proof.
dca by have := leq_dsum_alpha_2l_l 1 n; rewrite addn1. Qed.


(* This is 3.7 *)
Lemma alpha_4_3 n : 3 < n -> 3 * α_[1] n.+1 <= 4 * α_[1] n.
7af
3 < n -> 3 * α_[1] n.+1 <= 4 * α_[1] n
Proof.
dcf
rewrite !alphaL1E.
7af
3 < n -> 3 * α n.+1 <= 4 * α n
move=> n_gt_3.
19
n_gt_3:3 < n
3 * α n.+1 <= 4 * α n
have an_gt_5 : 5 < α n by apply: increasingE (increasing_alpha) n_gt_3.
19ddb
an_gt_5:5 < α n
ddc
have [[i [|j]] /= anE] : isAB 2 3 (α n) by apply: isAB_alpha.
19ddbde137
anE:α n = 2 ^ i * 3 ^ 0
ddc
19ddbde1
i, j:nat
anE:α n = 2 ^ i * 3 ^ j.+1
ddc
  rewrite muln1 in anE.
19ddbde137
anE:α n = 2 ^ i
ddc
de7
  case: i anE an_gt_5 => [|[|[|i anE an_gt_5]]]; try by move=> ->.
19ddb37
anE:α n = 2 ^ i.+3
de1
ddc
de7
  suff H1 : 8 * α n.+1 <= 9 * α n.
19ddb37df5de1
H1:8 * α n.+1 <= 9 * α n
ddc
df4
8 * α n.+1 <= 9 * α n
de8
    rewrite -3!leq_double -!mul2n !mulnA -[_ * 3]/(3 * 8).
df9
3 * 8 * α n.+1 <= 2 * 2 * 2 * 4 * α n
dfb
    apply: leq_trans (_ : (3 * 9) * α n <= _).
df9
3 * 8 * α n.+1 <= 3 * 9 * α n
df9
3 * 9 * α n <= 2 * 2 * 2 * 4 * α n
dfcde8
      by rewrite -!mulnA leq_mul2l //.
df9
e08
dfb
    by rewrite leq_mul2r orbT.
df4
dfd
de7
  pose m := 2 ^ i * 3 ^ 2.
19ddb37df5de1
m:=2 ^ i * 3 ^ 2:nat
dfd
de7
  case: (alpha_surjective (isT : 1 < 2) (isT : 2 < 3) (isT : coprime 2 3) i 2)
    => m1 m1H.
19ddb37df5de1e13
m1:nat
m1H:α m1 = 2 ^ i * 3 ^ 2
dfd
de7
  have H2 : α n < α m1.
e17
α n < α m1
19ddb37df5de1e13e18e19
H2:α n < α m1
dfd
de8
    by rewrite anE m1H !expnSr -!mulnA ltn_mul2l ?expn_gt0.
e20
dfd
de7
  have H3 : α n.+1 <= α m1.
e20
α n.+1 <= α m1
19ddb37df5de1e13e18e19e21
H3:α n.+1 <= α m1
dfd
de8
    case: (leqP m1 n) => /(increasingE increasing_alpha) //.
e20
α m1 <= α n -> α n.+1 <= α m1
e29
    by rewrite leqNgt H2.
e2b
dfd
de7
  rewrite anE !expnS [X in _ <= X]mulnC !mulnA -[2 * 2 * 2]/8 -mulnA leq_mul2l.
e2b
(8 == 0) || (α n.+1 <= 2 ^ i * 9)
de7
  by rewrite  -m1H.
de9
ddc
pose m := 2 ^ i.+2 * 3 ^ j.
19ddbde1deadeb
m:=2 ^ i.+2 * 3 ^ j:nat
ddc
case: (alpha_surjective (isT : 1 < 2) (isT : 2 < 3) (isT : coprime 2 3) i.+2 j)
    => m1 m1H.
19ddbde1deadebe3fe18
m1H:α m1 = 2 ^ i.+2 * 3 ^ j
ddc
have H2 : α n < α m1.
e43
e1d
19ddbde1deadebe3fe18e44e21
ddc
  rewrite anE m1H !expnSr -!mulnA ltn_mul2l ?expn_gt0 //=.
e43
3 ^ j * 3 < 2 * (2 * 3 ^ j)
e48
  by rewrite mulnC !mulnA ltn_mul2r ?expn_gt0.
e4a
ddc
have H3 : α n.+1 <= α m1.
e4a
e28
19ddbde1deadebe3fe18e44e21e2c
ddc
  case: (leqP m1 n) => /(increasingE increasing_alpha) //.
e4a
e30
e55
  by rewrite leqNgt H2.
e57
ddc
by rewrite anE !expnSr -[4]/(2 ^ 2) !mulnA -expnD add2n -m1H mulnC leq_mul2r.
Qed.

Lemma alphaL_1_2 n : α_[1] (n.+1) <= (α_[1] n).*2.
7af
α_[1] n.+1 <= (α_[1] n).*2
Proof.
e5f 
rewrite !alphaL1E.
7af
α n.+1 <= (α n).*2
case: n => // [] [|[|[|]]] // k.
9e1
α k.+1.+4 <= (α k.+4).*2
rewrite -(leq_pmul2l (_ : 0 < 3)) //.
9e1
3 * α k.+1.+4 <= 3 * (α k.+4).*2
rewrite -!alphaL1E.
9e1
3 * α_[1] k.+1.+4 <= 3 * (α_[1] k.+4).*2
apply: leq_trans (alpha_4_3 _) _ => //.
9e1
4 * α_[1] k.+4 <= 3 * (α_[1] k.+4).*2
by rewrite -mul2n mulnA leq_mul2r orbT.
Qed.

Lemma alphaL_4_5 n : α_[1] (n.+2) <= (α_[1] n).*2.+1.
7af
α_[1] n.+2 <= (α_[1] n).*2.+1
Proof.
e78 
rewrite !alphaL1E.
7af
α n.+2 <= (α n).*2.+1
case: n => // [] [|[|[|]]] // k.
9e1
α k.+2.+4 <= (α k.+4).*2.+1
rewrite -!alphaL1E.
9e1
α_[1] k.+2.+4 <= (α_[1] k.+4).*2.+1
apply: leq_trans (leqnSn _).
9e1
α_[1] k.+2.+4 <= (α_[1] k.+4).*2
rewrite -(leq_pmul2l (_ : 0 < 3)) //.
9e1
3 * α_[1] k.+2.+4 <= 3 * (α_[1] k.+4).*2
apply: leq_trans (alpha_4_3 _) _ => //.
9e1
4 * α_[1] k.+1.+4 <= 3 * (α_[1] k.+4).*2
rewrite -(leq_pmul2l (_ : 0 < 3)) //.
9e1
3 * (4 * α_[1] k.+1.+4) <= 3 * (3 * (α_[1] k.+4).*2)
rewrite mulnCA (leq_trans (_ : _ <= 4 * (4 *  α_[1] k.+4))) //.
9e1
4 * (3 * α_[1] k.+1.+4) <= 4 * (4 * α_[1] k.+4)
9e1
4 * (4 * α_[1] k.+4) <= 3 * (3 * (α_[1] k.+4).*2)
  by rewrite leq_mul2l /= alpha_4_3.
9e1
e9e
by rewrite -mul2n !mulnA leq_mul2r orbT.
Qed.

Lemma dsum_alphaL_S l n : S_[l] n.+1 = S_[l] n + α_[l] n.
8b1
S_[l] n.+1 = S_[l] n + α_[l] n
Proof.
ea3 by rewrite addnC subnK //; case: (convex_dsum_alphaL l). Qed.

Lemma dsum_alphaLE l n : S_[l] n = \sum_(i < n) α_[l] i.
8b1
S_[l] n = \sum_(i < n) α_[l] i
Proof.
ea8
elim: n => [|n IH].
909
S_[l] 0 = \sum_(i < 0) α_[l] i
8b2
IH:S_[l] n = \sum_(i < n) α_[l] i
S_[l] n.+1 = \sum_(i < n.+1) α_[l] i
  by rewrite /dsum_alphaL /conv /= dsum_alpha_0 muln0 big_ord0.
eb2
eb4
by rewrite dsum_alphaL_S IH big_ord_recr.
Qed.


(* Table *)

Lemma S1_small : 
  ((S_[1] 0 = 0) * (S_[1] 1 = 1) * (S_[1] 2 = 3) * (S_[1] 3 = 6) * 
  (S_[1] 4 = 10) * (S_[1] 5 = 16) * (S_[1] 6 = 24))%type.
((S_[1] 0 = 0) * (S_[1] 1 = 1) * (S_[1] 2 = 3) *
 (S_[1] 3 = 6) * (S_[1] 4 = 10) * (S_[1] 5 = 16) *
 (S_[1] 6 = 24))%type
Proof.
eb9
by rewrite /dsum_alphaL /conv /= /dsum_alpha
              -!(big_mkord xpredT) unlock /=; compute.
Qed.

Lemma S2_small : 
  ((S_[2] 0 = 0 ) * (S_[2] 1 = 2) * (S_[2] 2 = 4) * (S_[2] 3 = 8) * (
  S_[2] 4 = 14) * (S_[2] 5 = 20) * (S_[2] 6 = 28))%type.
((S_[2] 0 = 0) * (S_[2] 1 = 2) * (S_[2] 2 = 4) *
 (S_[2] 3 = 8) * (S_[2] 4 = 14) * (S_[2] 5 = 20) *
 (S_[2] 6 = 28))%type
Proof.
ebe
by rewrite /dsum_alphaL /conv /= /dsum_alpha
              -!(big_mkord xpredT) unlock /=; compute.
Qed.

Lemma S3_small : 
  ((S_[3] 0 = 0) * (S_[3] 1 = 2) * (S_[3] 2 = 5) * (S_[3] 3 = 9) * (
  S_[3] 4 = 15) * (S_[3] 5 = 23) * (S_[3] 6 = 32))%type.
((S_[3] 0 = 0) * (S_[3] 1 = 2) * (S_[3] 2 = 5) *
 (S_[3] 3 = 9) * (S_[3] 4 = 15) * (S_[3] 5 = 23) *
 (S_[3] 6 = 32))%type
Proof.
ec3
by rewrite /dsum_alphaL /conv /= /dsum_alpha
              -!(big_mkord xpredT) unlock /=; compute.
Qed.

Lemma S4_small : 
  ((S_[4] 0 = 0) * (S_[4] 1 = 2) * (S_[4] 2 = 6) * (S_[4] 3 = 10) * (
  S_[4] 4 = 16) * (S_[4] 5 = 24) * (S_[4] 6 = 36))%type.
((S_[4] 0 = 0) * (S_[4] 1 = 2) * (S_[4] 2 = 6) *
 (S_[4] 3 = 10) * (S_[4] 4 = 16) * (S_[4] 5 = 24) *
 (S_[4] 6 = 36))%type
Proof.
ec8
by rewrite /dsum_alphaL /conv /= /dsum_alpha
              -!(big_mkord xpredT) unlock /=; compute.
Qed.

Lemma S5_small : 
  ((S_[5] 0 = 0) * (S_[5] 1 = 2) * (S_[5] 2 = 6) * (S_[5] 3 = 11) * (
  S_[5] 4 = 17) * (S_[5] 5 = 25) * (S_[5] 6 = 37))%type.
((S_[5] 0 = 0) * (S_[5] 1 = 2) * (S_[5] 2 = 6) *
 (S_[5] 3 = 11) * (S_[5] 4 = 17) * (S_[5] 5 = 25) *
 (S_[5] 6 = 37))%type
Proof.
ecd
by rewrite /dsum_alphaL /conv /= /dsum_alpha
              -!(big_mkord xpredT) unlock /=; compute.
Qed.

Lemma alpha1_small : 
  ((α_[1] 0 = 1) * (α_[1] 1 = 2) * (α_[1] 2 = 3) * (α_[1] 3 = 4) * 
  (α_[1] 4 = 6) * (α_[1] 5 = 8))%type.
((α_[1] 0 = 1) * (α_[1] 1 = 2) * (α_[1] 2 = 3) *
 (α_[1] 3 = 4) * (α_[1] 4 = 6) * (α_[1] 5 = 8))%type
Proof.
ed2
by rewrite /alphaL /delta !S1_small; compute.
Qed.

Lemma alpha2_small : 
  ((α_[2] 0 = 2) * (α_[2] 1 = 2) * (α_[2] 2 = 4) * (α_[2] 3 = 6) * (
  α_[2] 4 = 6) * (α_[2] 5 = 8))%type.
((α_[2] 0 = 2) * (α_[2] 1 = 2) * (α_[2] 2 = 4) *
 (α_[2] 3 = 6) * (α_[2] 4 = 6) * (α_[2] 5 = 8))%type
Proof.
ed7
by rewrite /alphaL /delta !S2_small; compute.
Qed.

Lemma alpha3_small : 
  ((α_[3] 0 = 2) * (α_[3] 1 = 3) * (α_[3] 2 = 4) * (α_[3] 3 = 6) * (
  α_[3] 4 = 8) * (α_[3] 5 = 9))%type.
((α_[3] 0 = 2) * (α_[3] 1 = 3) * (α_[3] 2 = 4) *
 (α_[3] 3 = 6) * (α_[3] 4 = 8) * (α_[3] 5 = 9))%type
Proof.
edc
by rewrite /alphaL /delta !S3_small; compute.
Qed.

Lemma alpha4_small : 
  ((α_[4] 0 = 2) * (α_[4] 1 = 4) * (α_[4] 2 = 4) * (α_[4] 3 = 6) * (
  α_[4] 4 = 8) * (α_[4] 5 = 12))%type.
((α_[4] 0 = 2) * (α_[4] 1 = 4) * (α_[4] 2 = 4) *
 (α_[4] 3 = 6) * (α_[4] 4 = 8) * (α_[4] 5 = 12))%type
Proof.
ee1
by rewrite /alphaL /delta !S4_small; compute.
Qed.

Lemma alpha5_small : 
  ((α_[5] 0 = 2) * (α_[5] 1 = 4) * (α_[5] 2 = 5) * (α_[5] 3 = 6) * (
  α_[5] 4 = 8) * (α_[5] 5 = 12))%type.
((α_[5] 0 = 2) * (α_[5] 1 = 4) * (α_[5] 2 = 5) *
 (α_[5] 3 = 6) * (α_[5] 4 = 8) * (α_[5] 5 = 12))%type
Proof.
ee6
by rewrite /alphaL /delta !S5_small; compute.
Qed.

Definition alphaS_small :=
   (S1_small, S2_small, S3_small, S4_small, S5_small).

Definition alpha_small :=
   (alpha1_small, alpha2_small, alpha3_small, alpha4_small, alpha5_small).

End S23.

Notation α := (alpha 2 3).

Notation "\min_ ( i <= n ) F" := (bigmin (fun i => F) n)
 (at level 41, F at level 41, i, n at level 50,
  format "\min_ ( i  <=  n )  F").

Notation " 'S_[' l ']' " := (dsum_alphaL l) 
 (format "S_[ l ]").

Notation " 'α_[' l ']' " := (alphaL l) 
 (format "α_[ l ]").

Notation S1 := dsum_alpha.