proposition: Lemma case3 l (u : {ffun 'I_l.+2 -> configuration 4 n.+2}) (p1 p2 p3: peg 4) : p1 != p2 -> p1 != p3 -> p2 != p3 -> p1 != p0 -> p2 != p0 -> p3 != p0 -> (forall k : 'I_l.+2, 0 < k < l.+1 -> codom (u k) \subset [:: p2; a[p1, p3] k]) -> (u ord0 ord_max = p1) -> (u ord_max ord_max = a[p3, p1] l) -> (S_[l.+1] n.+2).*2 <= sd u + sp (u ord0) l.+1 p1 + sp (u ord_max) l.+1 (a[p3, p1] l).
proof: Proof. move=> p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0. move=> cH KH1 KH2. pose u':= ([ffun i => ↓[u i]] : {ffun 'I_l.+2 -> configuration 4 n.+1}) : {ffun 'I_l.+2 -> configuration 4 n.+1}. have H: forall k : 'I_l.+2, 0 < k < l.+1 -> codom (u' k) \subset [:: p2; a[p1, p3] k]. by move=> k kH; rewrite ffunE; apply/codom_liftr/cH. have apegpaD2 a : a[p1, p3] a != p2. by rewrite /apeg; case: odd; rewrite // eq_sym. have apegpaD0 a : a[p1, p3] a != p0. by rewrite /apeg; case: odd; rewrite // eq_sym. case: (pickP (fun i => u i ldisk != a[p1, p3] i)) => [x xH|pH]; last first. have {pH}ukLE k : u k ldisk = a[p1, p3] k by have := pH k; case: eqP. have := case2 _ _ _ _ _ _ _ cH KH1 KH2 ukLE. by apply. have exH : exists x, u (inord x) ldisk != a[p1, p3] x. exists x; rewrite (_ : inord x = x) //. by apply/val_eqP; rewrite /= inordK. case: (@ex_minnP _ exH) => a aH {exH}aMin. have exL : exists x, (x <= l) && (u (inord x) ord_max != a[p1, p3] x). exists x; apply/andP; split => //. have := ltn_ord x. rewrite ltnS leq_eqVlt => /orP[] // /eqP xEl1. case/eqP: xH. rewrite (_ : x = ord_max); last by apply/val_eqP/eqP. by apply/eqP/val_eqP; rewrite /= apegS. by rewrite (_ : inord x = x) //; apply/val_eqP; rewrite /= inordK. have exL1 y : (y <= l) && (u (inord y) ord_max != a[p1, p3] y) -> y <= l. by case/andP. pose a1 := ex_maxn exL exL1. have a1H: u (inord a1) ldisk != a[p1, p3] a1. by rewrite /a1; case: ex_maxnP => i /andP[]. have a1Ll : a1 <= l by rewrite /a1; case: ex_maxnP => i /andP[]. have a1Max i : a1 < i < l.+2 -> u (inord i) ord_max = a[p1, p3] i. case/andP=> a1Li; rewrite ltnS leq_eqVlt => /orP[/eqP iEl1|iLl]. rewrite iEl1 apegS (_ : inord l.+1 = ldisk) //. by apply/val_eqP; rewrite /= inordK. move: a1Li; rewrite /a1; case: ex_maxnP => j _ /(_ i). by case: eqP; rewrite // andbT => _ /(_ iLl); rewrite ltnNge => ->. have aLld1 : a <= l.+1. rewrite -ltnS; apply: leq_trans (ltn_ord x). rewrite ltnS; apply: aMin;rewrite (_ : inord x = x) //. by apply/val_eqP; rewrite /= inordK. wlog aLl1Ba1 : u p1 p3 p1Dp3 p2Dp3 p3Dp0 apegpaD2 apegpaD0 p1Dp2 p1Dp0 {u' H xH exL exL1}cH KH1 KH2 a a1 aH aLld1 aMin a1H a1Ll a1Max / a <= l.+1 - a1. move=> wH. case: (leqP a (l.+1 -a1)) => [aLl1Ba1|l1Ba1La]. by apply: wH aLl1Ba1. have a_gt0 : 0 < a by apply: leq_ltn_trans l1Ba1La. pose u1 : {ffun 'I_l.+2 -> configuration 4 n.+2} := [ffun i : 'I_l.+2 => u (inord (l.+1 - i))]. have -> : sd u = sd u1. have F : injective (fun i : 'I_l.+1 => (inord (l - i) : 'I_l.+1)). move=> i j /val_eqP. have lBiLl (i1 : 'I_l.+1) : l - i1 < l.+1. by rewrite ltn_subLR ?leq_addl // -ltnS. rewrite /= !inordK // => /eqP liE; apply/val_eqP => /=. rewrite -(subKn (_ : i <= l)); last by rewrite -ltnS. by rewrite liE subKn // -ltnS. rewrite [sd u](reindex_inj F) /=. apply: eq_bigr => i _; rewrite !ffunE. have iLl2 : i < l.+2 by apply: leq_trans (ltn_ord _) _. have lBiLl : l - i < l.+1 by rewrite ltn_subLR ?leq_addl // -ltnS. have iLl : i <= l by rewrite -ltnS. rewrite gdistC; last by apply/move_sym/ssym. congr (`d[u _,u _]_smove). by apply/val_eqP; rewrite /= !inordK ?subSn. by apply/val_eqP; rewrite /= !inordK // ?subSS ltnS // ltnW. pose p1' := a[p1, p3] l; pose p3' := a[p3, p1] l. have -> : sp (u ord0) l.+1 p1 = sp (u1 ord_max) l.+1 (a[p1', p3'] l). apply: eq_bigr => i _; congr (_ * _). rewrite -apegD addnn apegO odd_double /= apegS apeg0. by rewrite ffunE subnn inord_eq0. have -> : sp (u ord_max) l.+1 (a[p3, p1] l) = sp (u1 ord0) l.+1 p3'. apply: eq_bigr => i _; congr (_ * _). rewrite ffunE subn0. suff -> : inord l.+1 = ord_max :> 'I_l.+2 by []. by apply/val_eqP; rewrite /= inordK. rewrite addnAC. have FF : (l.+1 - a1) <= l.+1 - (l.+1 - a). by rewrite leq_sub2l // leq_subLR addnC -leq_subLR ltnW. have a1Ll1 : a1 <= l.+1 by rewrite (leq_trans a1Ll). apply: wH FF => //. - by rewrite apeg_eqC eq_sym. - by rewrite eq_sym apeg_neq // eq_sym. - by rewrite apeg_neq // eq_sym. - by move=> b; rewrite !apeg_neq // eq_sym. - by move=> b; rewrite !apeg_neq // eq_sym. - by rewrite apeg_neq // eq_sym. - by rewrite apeg_neq // eq_sym. - move=> k /andP[kH1 kH2]; rewrite ffunE. have F1 : k <= l.+1 by apply: ltnW. have F2 : l.+1 - k < l.+2. by rewrite ltn_subLR // addnS ltnS leq_addl. have -> : a[p3', p1'] k = a[p1, p3] (inord (l.+1 - k) : 'I_l.+2) . rewrite inordK // -apegD -apegS -addnS. by rewrite [LHS]apegO [RHS]apegO oddD oddB //= addbC. apply: cH; rewrite inordK // subn_gt0 // ltn_subLR // kH2 //=. by rewrite addnS ltnS -{1}[l.+1]add1n leq_add2r. - rewrite !ffunE /p1' subn0 -[RHS]KH2; congr (u _ _); apply/val_eqP. by rewrite /= inordK. - by rewrite !ffunE /p1' subnn inord_eq0 // KH1 /p3' -apegD addnn apeg_double. - rewrite ffunE inordK //=; last by rewrite ltnS leq_subr. rewrite subKn // -apegD apegO oddD oddB //= addbAC !addNb addbb /=. by rewrite -oddS -apegO apegS. - by rewrite leq_subr. - move=> k; rewrite ffunE. case: leqP => //; rewrite ltn_subRL addnC -ltn_subRL => kH. have kLl1 : k < l.+1 by rewrite -subn_gt0 (leq_ltn_trans _ kH). rewrite inordK; last by rewrite ltnS ltnW. have /a1Max-> : a1 < l.+1 - k < l.+2 by rewrite kH /= ltnS leq_subr. case/eqP; rewrite -apegD apegO oddB 1?ltnW // -oddD -apegO. by rewrite addSn addnC apegS. - rewrite ffunE inordK ?ltnS ?leq_subr //. rewrite subKn //. rewrite -apegD apegO oddD oddB //= !addNb addbAC addbb /=. by rewrite -oddS -apegO apegS. - by rewrite -[a]prednK // subSS leq_subr. move=> k /andP[l1BaLk kLl2]; rewrite ffunE. rewrite inordK //; apply/eqP; case: eqP => // /eqP. suff -> : a[p3', p1'] k = a[p1, p3] (l.+1 - k). by move=> /aMin; rewrite leqNgt ltn_subLR // addnC -ltn_subLR // l1BaLk. by rewrite [RHS]apegO oddB // -oddD -apegO addSn apegS addnC apegD. pose u':= ([ffun i => ↓[u i]] : {ffun 'I_l.+2 -> configuration 4 n.+1}) : {ffun 'I_l.+2 -> configuration 4 n.+1}. have H: forall k : 'I_l.+2, 0 < k < l.+1 -> codom (u' k) \subset [:: p2; a[p1, p3] k]. by move=> k kH; rewrite ffunE; apply/codom_liftr/cH. have aMin1 i : i < a -> u (inord i) ord_max = a[p1, p3] i. by case: (u (inord i) ord_max =P a[p1, p3] i) => // /eqP /aMin; case: leqP. have a_gt0 : 0 < a. have : 0 <= a by []. rewrite leq_eqVlt => /orP[/eqP aE0|] //. by case/eqP: aH; rewrite inord_eq0 // -aE0. pose ai : 'I_l.+2 := inord a. have aiE : ai = a :> nat by rewrite inordK. have aLa1 : a <= a1. case: leqP => // => a1La. by case/eqP: aH; apply: a1Max; rewrite a1La. have uaLEp2 : u (inord a) ldisk = p2. have /cH : 0 < (inord a : 'I_l.+2) < l.+1. by rewrite inordK // a_gt0 /= (leq_ltn_trans _ (_ : a1 < l.+1)). move=> /subsetP/(_ (u (inord a) ldisk) (codom_f _ _)). by rewrite !inE inordK // (negPf aH) orbF => /eqP. have ua1LEp2 : u (inord a1) ldisk = p2. have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1. by rewrite inordK // !ltnS (leq_trans a1Ll) // (leq_trans a_gt0). move=> /subsetP/(_ (u (inord a1) ldisk) (codom_f _ _)). by rewrite !inE inordK ?ltnS ?(leq_trans a1Ll) // (negPf a1H) orbF => /eqP. have a1_gt0 : 0 < a1 by apply: leq_trans a_gt0 _. pose b := a1 - a. pose c := l.+1 - a1. have c_gt0 : 0 < c by rewrite subn_gt0. have l1E : l.+1 = a + b + c. by rewrite /b /c [a + _]addnC subnK // addnC subnK // ltnW. pose si i : configuration 4 n.+1 := sgdist1 p2 (u (inord i)) (u (inord i.+1)). pose ti i : configuration 4 n.+1 := sgdist2 p2 (u (inord i)) (u (inord i.+1)). have sitiH i : i < a.-1 -> [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ], codom (ti i) \subset [:: u (inord i) ldisk; p2] & `d[u (inord i), u (inord i.+1)]_smove = D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2]. move=> iLa. have iLa1 : i < a by rewrite (leq_trans iLa) // ssrnat.leq_pred. apply: sgdistE; rewrite ?aMin1 // -1?[a]prednK //. by rewrite apegS apeg_eqC. by rewrite eq_sym. pose pa := a[p1, p3] a. pose sam1 : configuration 4 n.+1 := sgdist1 pa (u (inord a.-1)) (u (inord a)). pose tam1 : configuration 4 n.+1 := sgdist2 pa (u (inord a.-1)) (u (inord a)). have [sam1C tam1C duam1ua1E] : [/\ codom sam1 \subset [:: pa; u (inord a) ldisk ], codom tam1 \subset [:: u (inord a.-1) ldisk; pa] & `d[u (inord a.-1), u (inord a)]_smove = D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2]. apply: sgdistE; rewrite /pa ?uaLEp2 ?aMin1 ?prednK //. by rewrite -{2}(prednK a_gt0) apegS apeg_eqC. rewrite uaLEp2 in sam1C. have {}tam1C : codom tam1 \subset [:: p1; p3]. move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK. by rewrite /pa -{2}[a]prednK // apegS codom_apeg. pose u1 := [ffun i : 'I_(3 * a).+1 => if (i %% 3) == 0 then ↓[u (inord (i %/ 3))] else if (i %% 3) == 1 then (if i == (3 * a.-1).+1 :> nat then sam1 else si (i %/ 3)) else (if i == (3 * a.-1).+2 :> nat then tam1 else ti (i %/ 3))]. have u10E : u1 ord0 = ↓[u ord0] by rewrite ffunE /= inord_eq0. have uiME : u1 ord_max = ↓[u (inord a)] by rewrite ffunE /= mod3E /= div3E. have P1 : a.*2 + sd u1 = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove. rewrite /sd. have -> := @sum3E _ (fun i => `d[u1 (inord i), u1 (inord i.+1)]_smove). have -> : a.*2 = \sum_(i < a) 2. by rewrite sum_nat_const /= cardT size_enum_ord muln2. rewrite -big_split /=. apply: eq_bigr => i _. have -> : u1 (inord (3 * i)) = ↓[u (inord i)]. rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /= ltnW. by rewrite mod3E /= div3E. have -> : u1 (inord (3 * i).+3) = ↓[u (inord i.+1)]. rewrite -[(_ * _).+3](mulnDr 3 1). rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /=. by rewrite mod3E /= div3E. have [/eqP iEa| iDa] := boolP (i == a.-1 :> nat). have -> : u1 (inord (3 * i).+1) = sam1. rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=. rewrite mod3E /= div3E. by rewrite iEa eqxx. have -> : u1 (inord (3 * i).+2) = tam1. rewrite ffunE inordK; last first. by rewrite -[_.+3](mulnDr 3 1) ltnW // add1n ltnS leq_mul2l /=. rewrite mod3E /= div3E. by rewrite iEa eqxx. by rewrite iEa prednK // duam1ua1E /= -!addnA add2n !addnA addn0. have -> : u1 (inord (3 * i).+1) = si i. rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=. rewrite mod3E /= div3E. by rewrite [_.+1 == _.+1]eqn_mul2l /= (negPf iDa). have -> : u1 (inord (3 * i).+2) = ti i. rewrite ffunE inordK; last first. by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS add1n leq_mul2l /=. rewrite mod3E /= div3E. by rewrite [_.+1 == _.+1]eqn_mul2l /= (negPf iDa). case: (sitiH i) => // [|_ _ ->]. rewrite -ltnS prednK //. have := ltn_ord i; rewrite leq_eqVlt => /orP[] //. by rewrite -{2}[a]prednK // [_ == _](negPf iDa). by rewrite /= -!addnA add2n addn0. have sitiHb i : a1 < i < l.+1 -> [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ], codom (ti i) \subset [:: u (inord i) ldisk; p2] & `d[u (inord i), u (inord i.+1)]_smove = D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2]. move=> /andP[a1Li iLl]. apply: sgdistE => //; rewrite !a1Max ?a1Li ?(leq_trans a1Li) // ?(leq_trans iLl) //. by rewrite apegS apeg_eqC. by rewrite eq_sym. pose sa1 : configuration 4 n.+1 := sgdist1 (a[p1, p3] a1) (u (inord a1)) (u (inord a1.+1)). pose ta1 : configuration 4 n.+1 := sgdist2 (a[p1, p3] a1) (u (inord a1)) (u (inord a1.+1)). have [sa1C ta1C dua1uad1E] : [/\ codom sa1 \subset [:: a[p1, p3] a1; u (inord a1.+1) ldisk ], codom ta1 \subset [:: u (inord a1) ldisk; a[p1, p3] a1] & `d[u (inord a1), u (inord a1.+1)]_smove = D[[:: ↓[u (inord a1)]; sa1 ; ta1; ↓[u (inord a1.+1)]]].+2]. apply: sgdistE; rewrite ?ua1LEp2 ?a1Max ?leqnn // 1?eq_sym //. by rewrite apegS apeg_eqC eq_sym. rewrite ua1LEp2 in ta1C. have {}sa1C : codom sa1 \subset [:: p1; p3]. move: sa1C; rewrite a1Max //; last by rewrite leqnn. by rewrite apegS codom_apeg. pose u2 := [ffun i : 'I_(3 * c).+1 => if (i %% 3) == 0 then ↓[u (inord (a1 +(i %/ 3)))] else if (i %% 3) == 1 then (if i == 1 :> nat then sa1 else si (a1 + (i %/ 3))) else (if i == 2 :> nat then ta1 else ti (a1 + (i %/ 3)))]. have u20E : u2 ord0 = ↓[u (inord a1)] by rewrite ffunE /= addn0. have u2ME : u2 ord_max = ↓[u ord_max]. rewrite ffunE /= mod3E /= div3E addnC subnK //. by rewrite (_ : inord _ = ord_max) //; apply/val_eqP; rewrite /= inordK. by rewrite ltnW // ltnS. have P2 : c.*2 + sd u2 = \sum_(a1 <= i < l.+1) `d[u (inord i), u (inord i.+1)]_smove. have -> : \sum_(a1 <= i < l.+1) `d[u (inord i), u (inord i.+1)]_smove = \sum_(i < c) `d[u (inord (a1 + i)), u (inord (a1 + i).+1)]_smove. rewrite -{1}[a1]add0n big_addn big_mkord. by apply: eq_bigr => i _; rewrite addnC. rewrite /sd. have -> := @sum3E _ (fun i => `d[u2 (inord i), u2 (inord i.+1)]_smove). have -> : c.*2 = \sum_(i < c) 2. by rewrite sum_nat_const /= cardT size_enum_ord muln2. rewrite -big_split /=. apply: eq_bigr => i _. have -> : u2 (inord (3 * i)) = ↓[u (inord (a1 + i))]. rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /= ltnW. by rewrite mod3E /= div3E. have -> : u2 (inord (3 * i).+3) = ↓[u (inord (a1 + i).+1)]. rewrite -[(_ * _).+3](mulnDr 3 1). rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /=. by rewrite mod3E /= div3E // add1n addnS. have [/eqP iEa| iDa] := boolP (i == 0 :> nat). have -> : u2 (inord (3 * i).+1) = sa1. rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=. rewrite mod3E /=. by rewrite iEa eqxx. have -> : u2 (inord (3 * i).+2) = ta1. rewrite ffunE inordK; last first. by rewrite -[_.+3](mulnDr 3 1) ltnW // add1n ltnS leq_mul2l /=. rewrite mod3E /=. by rewrite iEa eqxx. by rewrite iEa !addn0 // dua1uad1E /= -!addnA add2n !addnA addn0. have -> : u2 (inord (3 * i).+1) = si (a1 + i). rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=. rewrite mod3E /= div3E. by rewrite [_.+1 == _.+1](eqn_mul2l 3 _ 0) /= (negPf iDa). have -> : u2 (inord (3 * i).+2) = ti (a1 + i). rewrite ffunE inordK; last first. by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS add1n leq_mul2l /=. rewrite mod3E /= div3E. by rewrite [_.+1 == _.+1](eqn_mul2l 3 _ 0) /= (negPf iDa). case: (sitiHb (a1 + i)) => // [|_ _ ->]. rewrite -addn1 leq_add2l lt0n iDa /= -[l.+1](subnK (_ : a1 <= l.+1)). by rewrite addnC ltn_add2r. by rewrite ltnW. by rewrite /= -!addnA add2n addn0. have P3 : \sum_(a <= i < a1) `d[↓[u (inord i)], ↓[u (inord i.+1)]]_smove <= \sum_(a <= i < a1) `d[u (inord i), u (inord i.+1)]_smove. apply: leq_sum => i _. by apply: gdist_cunlift; apply: shanoi_connect. have SH : 2 <= l -> (S_[l.+1] n.+2).*2 <= S_[l.+1] n.+2 + S_[l] n.+1 + (α_[1] n.+1).*2. move=> l_gt2. rewrite -addnn -!addnA leq_add2l. by apply: dsum_alphaL_alpha. have [/andP[a_gt1 c_gt1]|] := boolP ((1 < a) && (1 < c)). have l_gt0 : 0 < l by rewrite -ltnS l1E (leq_trans c_gt1) // leq_addl. rewrite !sum_beta_S //= KH1 KH2 !eqxx !addn0. pose u1l := [ffun i : 'I_(3 * a).-2.+1 => u1 (inord i)]. have a3_gt1 : 1 < (3 * a).-2 by rewrite -(subnK a_gt1) addn2 !mulnS. have c3_gt1 : 1 < (3 * c).-2 by rewrite -(subnK c_gt1) addn2 !mulnS. have cH1 (k : 'I_(3 * a).-2.+1) : 0 < k < (3 * a).-2 -> codom (u1l k) \subset [:: p2; a[p1, p3] k]. move=> /andP[k_gt0 k3L3a]. have k3La1 : k %/ 3 <= a.-1. have kL3a : k <= 3 * (a.-1). rewrite -[a.-1]subn1 mulnBr -ltnS -[3 *1]/(2.+1) subnSK. by rewrite subn2. by rewrite (leq_mul2l 3 1). by rewrite -[a.-1](mulKn _ (_ : 0 < 3)) // leq_div2r. have k3Ll : k %/ 3 < l. rewrite -ltnS l1E (leq_trans (_ : _ < a.-1.+3)) //; last first. rewrite prednK // addnAC -addn2 (leq_trans (_ : _ <= a + c)) //. by rewrite leq_add2l. by rewrite leq_addr. by rewrite !ltnS ltnW // ltnS. rewrite !ffunE inordK //; last first. rewrite (leq_trans (ltn_ord _)) // -subn2 ltn_subLR. by rewrite add2n ltnS // ltnW. by rewrite (leq_trans (_ : _ < 3 * 1)) // leq_mul2l. rewrite {8}(divn_eq k 3) apegD [_ * 3]mulnC apegMr //=. case: eqP => [km3E0 /= |/eqP km3D0]. have k3_gt0 : 0 < k %/ 3. case: (k: nat) k_gt0 km3E0 => // [] [|[|k1 _ _]] //. by rewrite (divnMDl 1 k1 (_ : 0 < 3)). rewrite km3E0 !apeg0. have /H : 0 < (inord (k %/ 3) : 'I_l.+2) < l.+1. rewrite inordK //. by rewrite k3_gt0 /= (leq_trans k3Ll). by rewrite (leq_trans k3Ll) // ltnW. by rewrite ffunE inordK // (leq_trans k3Ll) // ltnW . case: eqP => [km3E1|/eqP km3D1]. rewrite km3E1 !apegS !apeg0; case: eqP => [->|kE3a1]. rewrite (_ : (3 * a.-1).+1 = a.-1 * 3 + 1); last by rewrite addn1 mulnC. rewrite divnMDl // divn_small // addn0. by have := sam1C; rewrite codom_subC /pa -{1}[a]prednK //= apegS. move: k3La1; rewrite leq_eqVlt => /orP[/eqP k3Ea1| k3La]. case: kE3a1. by rewrite (divn_eq k 3) km3E1 k3Ea1 mulnC addn1. case: (sitiH (k %/ 3)) => // siH _ _; move: siH. by rewrite aMin1 ?apegS // -{2}[a]prednK . have km3E2 : k %% 3 = 2. by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 => // [] [|[|]]. rewrite km3E2 !apegS !apeg0; case: eqP => [kE3a1|kD3a1]. rewrite ltnNge in k3L3a; case/negP: k3L3a. by rewrite kE3a1 -{1}[a]prednK // mulnS. move: k3La1; rewrite leq_eqVlt => /orP[/eqP k3Ea1| k3La]. case: kD3a1. by rewrite (divn_eq k 3) km3E2 k3Ea1 mulnC addn2. rewrite codom_subC. case: (sitiH (k %/ 3)) => // _ tiH _; move: tiH. by rewrite aMin1 // -{2}[a]prednK // ltnS ltnW. have {cH1}P4 : (S_[(3 * a).-2] n.+1).*2 <= \sum_(i < (3 * a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove + \sum_(k < n.+1) (↓[u ord0] k != p1) * β_[n.+1, (3 * a).-2] k + \sum_(k < n.+1) (sam1 k != pa) * β_[n.+1, (3 * a).-2] k. apply: leq_trans (IH _ _ _ _ _ _ cH1) _ => //. rewrite leq_eqVlt; apply/orP; left; apply/eqP. congr (_ + _ + _); apply: eq_bigr => i _. - by rewrite ![u1l _]ffunE !inordK // ltnS // ltnW. - by rewrite ffunE inord_eq0 // ffunE /= inord_eq0. rewrite !ffunE /= inordK //; last first. by rewrite ltnS -subn2 leq_subr. rewrite (_ : _.-2 = (3 * a.-1).+1); last first. by rewrite -{1}[a]prednK // mulnS. rewrite mod3E /= eqxx. by rewrite /pa apegS apegMr //= -apegS prednK. have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). set x1S := \sum_(_ < _.+1) _ in P4; set x2S := \sum_(_ < _.+1) _ in P4. rewrite -/x1S. pose u2r := [ffun i : 'I_(3 * c).-2.+1 => u2 (inord i.+2)]. pose pa1 := a[p1, p3] a1. pose pa1S := a[p1, p3] a1.+1. have cH1 (k : 'I_(3 * c).-2.+1) : 0 < k < (3 * c).-2 -> codom (u2r k) \subset [:: p2; a[pa1, pa1S] k]. move=> /andP[k_gt0 k3L3a]. have k2L3c : k.+2 < (3 * c). by have := k3L3a; rewrite -{2}subn2 ltn_subRL add2n. rewrite !ffunE inordK ?ltnS 1?ltnW //. case: eqP => [km3E0 /= |/eqP km3D0]. have k3_gt0 : 0 < k.+2 %/ 3. case: (k: nat) k_gt0 km3E0 => // [] //= k1 _ _. by rewrite (divnMDl 1 k1 (_ : 0 < 3)). have a1k3Ll1 : a1 + k.+2 %/ 3 < l.+1. move: k2L3c. rewrite {1}(divn_eq k.+2 3) km3E0 addn0 mulnC ltn_mul2l /= => k2L3c. rewrite -(subnK (_ : a1 <= l.+1)) ?(leq_trans a1Ll) //. by rewrite addnC ltn_add2r -/c. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2 %/ 3)) ; last first. rewrite /pa1 /pa1S apegS -apegD -2!apegS -!addSn addnC. rewrite {1}(divn_eq k.+2 3) km3E0 addn0 apegO. by rewrite oddD oddM andbT -oddD -apegO. have /H : 0 < (inord (a1 + k.+2 %/ 3) : 'I_l.+2) < l.+1. rewrite inordK; first by rewrite addn_gt0 a1_gt0. by rewrite ltnS ltnW. by rewrite ffunE inordK // ltnS ltnW. case: eqP => [km3E1|/eqP km3D1]. rewrite eqn_leq ltnNge /=. have a1La1k : a1 < a1 + k.+2 %/3. by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0. have a1k3Ll : a1 + k.+2 %/ 3 < l.+1. move: (ltnW k2L3c). rewrite {1}(divn_eq k.+2 3) km3E1 addn1 mulnC ltn_mul2l /=. rewrite -(subnK (_ : a1 <= l.+1)) ?(leq_trans a1Ll) //. by rewrite addnC ltn_add2r -/c. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first. by rewrite /pa1S apegS -apegD !addnS addnC !apegS. rewrite (_ : a[_, _ ] _ = a[p3, p1] (a1 + (k.+2) %/ 3)) ; last first. rewrite apegO oddD {1}(divn_eq k.+2 3) oddD km3E1 addbT oddM andbT. by rewrite addbN -oddD -oddS -apegO apegS. case: (sitiHb (a1 + k.+2 %/ 3)) => // [| siH _ _]. by rewrite a1La1k. by move: siH; rewrite a1Max ?apegS // ltnS ltnW. have km3E2 : k.+2 %% 3 = 2. by case: (_ %% _) (ltn_mod k.+2 3) km3D0 km3D1 => // [] [|[|]]. rewrite ifN; last by case: (k : nat) k_gt0. have a1La1k : a1 < a1 + k.+2 %/3. by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0. have a1k3Ll : a1 + k.+2 %/ 3 < l.+1. have: k.+2 %/ 3 * 3 < 3 * c. rewrite ltnW //. move: (ltnW k2L3c). by rewrite {1}(divn_eq k.+2 3) km3E2 addn2. rewrite mulnC ltn_mul2l /=. rewrite -(subnK (_ : a1 <= l.+1)) ?(leq_trans a1Ll) //. by rewrite addnC ltn_add2r -/c. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first. by rewrite /pa1 /pa1S apegS -apegD addnC !addnS !apegS. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first. rewrite apegO /= oddD {1}(divn_eq k.+2 3) !oddD oddM andbT. by rewrite km3E2 addbF -oddD -apegO. rewrite codom_subC. case: (sitiHb (a1 + k.+2 %/ 3)) => // [| _ tiH _]; first by rewrite a1La1k. by move: tiH; rewrite a1Max // a1La1k ltnS ltnW. have P5 : (S_[(3 * c).-2] n.+1).*2 <= \sum_(i < (3 * c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove + sp ta1 (3 * c).-2 pa1 + sp ↓[u ord_max] (3 * c).-2 (a[p3, p1] l). apply: leq_trans (IH _ _ _ _ _ _ cH1) _; rewrite /pa1 /pa1S {cH1}//. - by rewrite apegS apeg_eqC. - by rewrite eq_sym. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - apply: eq_bigr => i _. by rewrite ![u2r _]ffunE !inordK // ltnS // ltnW. - apply: eq_bigr => i _; congr ((_ != _) * _). rewrite !ffunE /= !inordK //=. by rewrite (leq_trans (_ : 2 < (3 * 1).+1)) // ltnS leq_mul2l. apply: eq_bigr => i _; congr ((_ != _) * _). rewrite !ffunE /= !prednK ?muln_gt0 //=; last first. by rewrite -subn1 ltn_subRL addn0 (leq_trans (_ : _ < 3 * 1)) // leq_mul2l. rewrite inordK // mod3E /= div3E addnC subnK; last first. by apply: (leq_trans a1Ll). by rewrite ffunE; congr (u _ _ ); apply/val_eqP; rewrite /= inordK. rewrite -[RHS]apegS -(subnK (_ : a1 <= l.+1)) // -/c. rewrite apegS -apegD apegO oddD -subn2 oddB. by rewrite addbF oddM /= -oddD -apegO. by rewrite (leq_trans (_ : _ < 3 * 1)) // leq_mul2l //. by rewrite ltnW. rewrite {cH1}//. have {}P5 := leq_trans P5 (leq_add (leqnn _) (leq_sum_beta _ _)). set y1S := \sum_(_ < _) _ in P5; set y2S := sp _ _ _ in P5. have [b_gt1|b_le2] := leqP 2 b. pose u3 := [ffun i : 'I_3 => if i == 0 :> nat then sam1 else if i == 1 :> nat then tam1 else ↓[u (inord a)]]. have cH6 (k : 'I_3) : 0 < k < 2 -> codom (u3 k) \subset [:: p1; a[p2, p3] k]. move=> /andP[k_gt0 k_lt2]. rewrite !ffunE. by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 => // [] [|]. have P6 : (S_[2] n.+1).*2 <= (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove) + sp sam1 2 p2 + sp ↓[u (inord a)] 2 p2. apply: (leq_trans (IH _ _ _ _ _ _ cH6)) => //. by rewrite eq_sym. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=. - by apply: eq_bigr => i _; rewrite !ffunE. by apply: eq_bigr => i _; rewrite !ffunE. rewrite {cH6}// in P6. set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6. have x2Sx3SE : x2S + x3S <= (S_[1] n).*2 + α_[maxn (3 * a).-2 2] n. by apply: sum_alpha_diffE; by rewrite /pa. rewrite (maxn_idPl _) // in x2Sx3SE. pose u4 := [ffun i : 'I_b.+1 => ↓[u (inord (a + i))]]. pose paS := a[p1, p3] a.+1. have cH7 (k : 'I_b.+1) : 0 < k < b -> codom (u4 k) \subset [:: p2; a[pa, paS] k]. move=> /andP[k_gt0 k_ltb]. have akLl : a + k < l.+1. rewrite ltnS (leq_trans _ a1Ll) //. by rewrite -(subnK aLa1) addnC leq_add2r ltnW. rewrite !ffunE. have /H : 0 < (inord (a + k) : 'I_l.+2) < l.+1. rewrite inordK; first by rewrite addn_gt0 a_gt0. by rewrite ltnS ltnW. rewrite ffunE inordK //; last by rewrite ltnS ltnW. by rewrite /pa /paS apegS -apegD [k + _]addnC. have P7 : (S_[b] n.+1).*2 <= \sum_(i < b) `d[↓[u (inord (a + i))], ↓[u (inord (a + i).+1)]]_smove + sp ↓[u (inord a)] b pa + sp ↓[u (inord a1)] b (a[p1, p3] a1). apply: leq_trans (IH _ _ _ _ _ _ cH7) (leq_add (leq_add _ _) _); rewrite /pa /paS // 1?eq_sym //. - by rewrite apegS apeg_eqC eq_sym. - apply: leq_sum => i; rewrite !ffunE !inordK ?addnS //. by rewrite ltnS. by rewrite ltnS ltnW. - by apply: leq_sum => i _; rewrite !ffunE addn0. apply: leq_sum => i _; rewrite !ffunE /= [a + b]addnC subnK //. by rewrite apegS -apegD subnK. set x4S := sp _ _ _ in P7; set y4S := sp _ _ _ in P7. have y3Sx4SE : y3S + x4S <= (S_[1] n).*2 + α_[maxn 2 b] n. apply: sum_alpha_diffE => //; first by rewrite /pa eq_sym. apply: codom_liftr. have := @cH (inord a); rewrite inordK //; apply. by rewrite a_gt0 /= ltnS (leq_trans _ a1Ll). rewrite (maxn_idPr _) // in y3Sx4SE. pose u5 := [ffun i : 'I_3 => if i == 0 :> nat then ↓[u (inord a1)] else if i == 1 :> nat then sa1 else ta1]. have cH8 (k : 'I_3) : 0 < k < 2 -> codom (u5 k) \subset [:: p1; a[p2, p3] k]. move=> /andP[k_gt0 k_lt2]. rewrite !ffunE. by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 => // [] [|]. have P8 : (S_[2] n.+1).*2 <= (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) + sp ↓[u (inord a1)] 2 p2 + sp ta1 2 p2. apply: (leq_trans (IH _ _ _ _ _ _ cH8)) => //; first by rewrite eq_sym. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=. - by apply: eq_bigr => i _; rewrite !ffunE. by apply: eq_bigr => i _; rewrite !ffunE. set x5S := sp _ _ _ in P8; set y5S := sp _ _ _ in P8. have y4Sx5SE : y4S + x5S <= (S_[1] n).*2 + α_[maxn b 2] n. apply: sum_alpha_diffE => //. apply: codom_liftr; rewrite codom_subC. have := @cH (inord a1); rewrite inordK //. by apply; rewrite a1_gt0 /= ltnS. by rewrite ltnS ltnW. rewrite (maxn_idPl _) // in y4Sx5SE. have y2Sy5SE : y2S + y5S <= (S_[1] n).*2 + α_[maxn (3 * c).-2 2] n. apply: sum_alpha_diffE => //; first by rewrite /pa1. by rewrite codom_subC. rewrite (maxn_idPl _) // in y2Sy5SE. rewrite (_ : sd u = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a <= i < a1) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a1 <= i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first. pose f i := `d[u (inord i), u (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f). by rewrite -!big_cat_nat //= ltnW. rewrite -{}P1 -{}P2. rewrite [X in _ <= _ + X + _ + _ + _ + _] (_ : _ = \sum_(i < (3 * a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove + `d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove); last first. pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f) . rewrite -{1}(subnK (_ : 1 < 3 * a)) //; last first. by rewrite -[a]prednK // mulnS. rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _). rewrite ffunE (_ : (3 * a).-2 = (3 * (a.-1)).+1); last first. by rewrite -{1}[a]prednK // mulnS. rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK. rewrite mod3E /= eqxx. rewrite ffunE inordK; last first. by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW. by rewrite mod3E /= eqxx. rewrite ffunE (_ : (3 * a).-2 = (3 * (a.-1)).+1); last first. by rewrite -{1}[a]prednK // mulnS. rewrite inordK; last first. by rewrite -{2}[a]prednK // mulnS. rewrite mod3E /= eqxx. rewrite ffunE inordK; last first. by rewrite -{2}[a]prednK // mulnS. by rewrite -[(_ * _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK. rewrite [X in _ <= _ + (_ + X) + _ + _] (_ : _ = `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove + \sum_(i < (3 * c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove); last first. pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f) . rewrite -{1}(subnK (_ : 1 < 3 * c)) //; last first. by rewrite -[c]prednK // mulnS. rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA; congr (_ + _ + _). - rewrite !ffunE !inordK ?addn0 //=. by rewrite ltnS muln_gt0. - rewrite !ffunE !inordK //=. by rewrite ltnW // ltnS (leq_mul2l 3 1 c). by rewrite ltnS muln_gt0. by rewrite big_mkord. rewrite -/y1S. set z1S := \sum_(_ < _) _; set z2S := \sum_(_ < _) _. set z3S := \sum_(_ <= _ < _) _. rewrite -/z1S in P4; rewrite -/z2S in P5; rewrite -/z3S in P3. rewrite -[z1S + _ + _]addnA; set d1 := `d[_,_]_ _ + `d[_,_]_ _; rewrite -/d1 in P6. set d2 := `d[_,_]_ _ + `d[_,_]_ _; rewrite -/d2 in P8. set xS := \sum_(_ <= _ < _) _ in P3. rewrite [X in _ <= X + _ + _](_ : _ = xS) in P7; last first. rewrite /xS -[in RHS](add0n a) big_addn -/b big_mkord. by apply: eq_bigr => i _; rewrite [a + _]addnC. have F1 := dsum_alphaL_S (3 * a).-2 n. have F2 := dsum_alphaL_S (3 * c).-2 n. have F3 := dsum_alphaL_S b n. have F4_a : 2 * a = 2 + a.-1 + a.-1. by rewrite -{1}[a]prednK // mul2n -addnn addnS. have F4_c : 2 * c = 2 + c.-1 + c.-1. by rewrite -{1}[c]prednK // mul2n -addnn addnS. have F4 i k : 0 < i -> S_[i.-1] k.+1 <= S_[(3 *i).-2] k + i.-1. move=> i_gt0; apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[i]prednK // mulnS addSn add2n /=. have F4an := F4 a n a_gt0. have F4an1 := F4 a n.+1 a_gt0. have F4cn := F4 c n (c_gt0). have F4cn1 := F4 c n.+1 (c_gt0). have l_gt1 : 1 < l. by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add. have F5 := SH l_gt1. have F6 : S_[l.+1] n.+2 + S_[1] n.+2 <= S_[a.-1] n.+2 + S_[(b + c).+2] n.+2. rewrite [X in _ <= X]addnC. rewrite (_ : l.+1 = 1 + a.-2 + (b + c).+1); last first. rewrite /b /c add1n -addSnnS !prednK //; last by rewrite -ltnS prednK. by rewrite addnCA addnA subnK // addnC subnK // ltnW. rewrite (_ : a.-1 = 1 + a.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F7 : S_[l] n.+1 + S_[1] n.+1 <= S_[a.-1] n.+1 + S_[(b + c).+1] n.+1. rewrite [X in _ <= X]addnC. rewrite (_ : l = 1 + a.-2 + (b + c)); last first. rewrite /b /c subSn // addnS -addSnnS add1n. rewrite !prednK //; last by rewrite -ltnS prednK. by rewrite addnCA addnA subnK // addnC subnK // ltnW. rewrite (_ : a.-1 = 1 + a.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). have F8 : S_[(b + c).+2] n.+2 + S_[1] n.+2 <= S_[c.-1] n.+2 + S_[b.+4] n.+2. rewrite (_ : (b + c).+2 = 1 + b.+3 + (c.-2)); last first. by rewrite add1n 2!addSnnS !prednK // -subn1 ltn_subRL addn0. rewrite (_ : c.-1 = 1 + c.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F9 : S_[(b + c).+1] n.+1 + S_[1] n.+1 <= S_[c.-1] n.+1 + S_[b.+3] n.+1. rewrite (_ : (b + c).+1 = 1 + b.+2 + (c.-2)); last first. by rewrite add1n 2!addSnnS !prednK // -subn1 ltn_subRL addn0. rewrite (_ : c.-1 = 1 + c.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). have F10 : S_[b.+4] n.+2 <= S_[b.+3] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha. have F11 : S_[b.+3] n.+1 <= S_[b.+2] n + (α_[1] n).*2. by apply: dsum_alphaL_alpha. have F12 : S_[b.+2] n + S_[1] n <= S_[b] n + S_[3] n. rewrite (_ : b.+2 = 1 + 2 + b.-1); last first. by rewrite add1n addSnnS prednK // ltnW. rewrite -{2}[b]prednK; last by apply: ltnW. by apply: concaveEk1 (concave_dsum_alphaL_l n). have F13 : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S. have F14 := leq_dsum_alpha_2l_1 n.+1. have F15n := dsum_alphaL_S 1 n.+1. have F15n1 := dsum_alphaL_S 1 n. move: P3 P4 P5 P6 P7 P8 => P3 P4 P5 P6 P7 P8. applyr P3. rewrite -(leq_add2r x2S); applyr P4. rewrite -(leq_add2r y2S); applyr P5. rewrite -(leq_add2r (x3S + y3S)); applyr P6. rewrite -(leq_add2r (x4S + y4S)); applyr P7. rewrite -(leq_add2r (x5S + y5S)); applyr P8. applyl y4Sx5SE; applyl y3Sx4SE; applyl y2Sy5SE; applyl x2Sx3SE. gsimpl. rewrite ![2 * S_[_.-2] _]mul2n -!addnn {1}F1 {1}F2. rewrite {F1 F2}F3; gsimpl. rewrite {}F4_a {}F4_c. applyr F4an; applyr F4an1; applyr F4cn; applyr F4cn1. applyl F5. rewrite -(leq_add2r (S_[1] n.+2)); applyl F6. rewrite -(leq_add2r (S_[1] n.+1)); applyl F7. rewrite -(leq_add2r (S_[1] n.+2)); applyl F8. rewrite -(leq_add2r (S_[1] n.+1)); applyl F9; gsimpl. applyl F10. changel ((4 * S_[1] n + (α_[1] n.+1).*2 + S_[b.+3] n.+1).*2). changer ((2 + S_[2] n.+1 + S_[b] n + S_[2] n.+1 + S_[1] n.+2 + (S_[1] n.+1)).*2). rewrite leq_double. applyl F11; applyl F12; gsimpl; applyr F14. rewrite -ltnS -!addnS -F13. by rewrite {}F15n {}F15n1; gsimpl. move: b_le2; rewrite leq_eqVlt => /orP[/eqP[] bE1|]. have a1E : a1 = a.+1 by rewrite -(subnK aLa1) -/b bE1. pose u3 := [ffun i : 'I_4 => if i == 0 :> nat then sam1 else if i == 1 :> nat then tam1 else if i == 2 :> nat then ↓[u (inord a)] else ↓[u (inord a.+1)]]. have cH6 (k : 'I_4) : 0 < k < 3 -> codom (u3 k) \subset [:: pa1S; a[p2, pa1] k]. move=> /andP[k_gt0 k_lt3]. rewrite !ffunE eqn_leq leqNgt k_gt0 /=. case: eqP => [->/=|/eqP kD1]. by rewrite /pa1S !apegS apeg0 codom_apeg codom_subC. have ->/= : k = 2 :> nat. by apply/eqP; rewrite eqn_leq -ltnS k_lt3 ltn_neqAle eq_sym k_gt0 kD1. apply: codom_liftr; rewrite codom_subC. have /cH : 0 < (inord a : 'I_l.+2) < l.+1. rewrite inordK //. by rewrite a_gt0 /= l1E bE1 addn1 leq_addr. by rewrite inordK // /pa1S a1E !apegS apeg0. have P6 : (S_[3] n.+1).*2 <= (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove + `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove) + sp sam1 3 p2 + sp ↓[u (inord a.+1)] 3 (a[p1, p3] a1). apply: (leq_trans (IH _ _ _ _ _ _ cH6)); rewrite /pa1S /pa1 //. - by rewrite eq_sym. - by rewrite eq_sym. - by rewrite apegS apeg_eqC eq_sym. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=. - by apply: eq_bigr => i _; rewrite !ffunE /=. by apply: eq_bigr => i _; rewrite !ffunE. set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6. have x2Sx3SE : x2S + x3S <= (S_[1] n).*2 + α_[maxn (3 * a).-2 3] n. by apply: sum_alpha_diffE; rewrite /pa. rewrite (maxn_idPl _) in x2Sx3SE; last first. by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2). pose u5 := [ffun i : 'I_3 => if i == 0 :> nat then ↓[u (inord a1)] else if i == 1 :> nat then sa1 else ta1]. have cH8 (k : 'I_3) : 0 < k < 2 -> codom (u5 k) \subset [:: p1; a[p2, p3] k]. move=> /andP[k_gt0 k_lt2]. rewrite !ffunE. by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 => // [] [|]. have P8 : (S_[2] n.+1).*2 <= (`d[↓[u (inord a.+1)], sa1]_smove + `d[sa1, ta1]_smove) + sp ↓[u (inord a.+1)] 2 p2 + sp ta1 2 p2. apply: (leq_trans (IH _ _ _ _ _ _ cH8)) => //. by rewrite eq_sym. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK //= a1E. - by apply: eq_bigr => i _; rewrite !ffunE a1E. by apply: eq_bigr => i _; rewrite !ffunE. set x5S := sp _ _ _ in P8; set y5S := sp _ _ _ in P8. have y3Sx5SE : y3S + x5S <= (S_[1] n).*2 + α_[3] n. apply: sum_alpha_diffE => //. apply: codom_liftr; rewrite codom_subC. have := @cH (inord a.+1); rewrite inordK ?a1E //. by apply; rewrite andTb //= ltnS -a1E. by rewrite -a1E ltnS ltnW. have y5Sy2SE : y5S + y2S <= (S_[1] n).*2 + α_[maxn 2 (3 * c).-2] n. by apply: sum_alpha_diffE; rewrite // /pa1 eq_sym. rewrite (maxn_idPr _) in y5Sy2SE; last first. by rewrite -subn2 ltn_subRL (ltn_mul2l 3 1). rewrite (_ : sd u = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a <= i < a1) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a1 <= i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first. pose f i := `d[u (inord i), u (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f). by rewrite -!big_cat_nat //= ltnW. rewrite -{}P1 -{}P2; applyr P3. rewrite (_ : sd u1 = \sum_(i < (3 * a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove + `d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove); last first. pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f) . rewrite -{1}(subnK (_ : 1 < 3 * a)) //; last first. by rewrite -[a]prednK // mulnS. rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _). rewrite ffunE (_ : (3 * a).-2 = (3 * (a.-1)).+1); last first. by rewrite -{1}[a]prednK // mulnS. rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK. rewrite mod3E /= eqxx. rewrite ffunE inordK; last first. by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW. by rewrite mod3E /= eqxx. rewrite ffunE (_ : (3 * a).-2 = (3 * (a.-1)).+1); last first. by rewrite -{1}[a]prednK // mulnS. rewrite inordK; last first. by rewrite -{2}[a]prednK // mulnS. rewrite mod3E /= eqxx. rewrite ffunE inordK; last first. by rewrite -{2}[a]prednK // mulnS. by rewrite -[(_ * _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK. rewrite (_ : sd u2 = `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove + \sum_(i < (3 * c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove); last first. pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f) . rewrite -{1}(subnK (_ : 1 < 3 * c)) //; last first. by rewrite -[c]prednK // mulnS. rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA. congr (_ + _ + _). - rewrite !ffunE !inordK ?addn0 //=. by rewrite ltnS muln_gt0. - rewrite !ffunE !inordK //=. by rewrite ltnW // ltnS (leq_mul2l 3 1 c). by rewrite ltnS muln_gt0. by rewrite big_mkord. rewrite (_ : \sum_(_ <= _ < _) _ = `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove); last first. by rewrite a1E big_nat1. set z1S := \sum_(_ < _) _ in P4; set z2S := \sum_(_ < _) _ in P5. rewrite -/z1S -/z2S. rewrite -a1E in P8; set d2 := `d[_,_]_ _ + `d[_,_]_ _ in P8; rewrite -/d2. set d1 := `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _ in P6. rewrite -/y1S. changer (2 * a + 2 * c + x1S + y1S + z1S + z2S + d2 + (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove + `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove)). rewrite -/d1. have F1 := dsum_alphaL_S (3 * a).-2 n. have F2 := dsum_alphaL_S (3 * c).-2 n. have F3 := dsum_alphaL_S 3 n. have F4_a : 2 * a = 2 + a.-1 + a.-1. by rewrite -{1}[a]prednK // mul2n -addnn addnS. have F4_c : 2 * c = 2 + c.-1 + c.-1. by rewrite -{1}[c]prednK // mul2n -addnn addnS. have F4 i k : 0 < i -> S_[i.-1] k.+1 <= S_[(3 *i).-2] k + i.-1. move=> i_gt0; apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[i]prednK // mulnS addSn add2n /=. have F4an := F4 a n a_gt0. have F4an1 := F4 a n.+1 a_gt0. have F4cn := F4 c n (c_gt0). have F4cn1 := F4 c n.+1 (c_gt0). have l_gt1 : 1 < l. by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add. have F5 := SH l_gt1. have F6n : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S. have F6n1 : S_[1] n.+2 = (S_[3] n.+1).+1 by rewrite dsum_alpha3_S. have am1_gt0 : 0 < a.-1 by rewrite -subn1 ltn_subRL addn0. have F7n1 : S_[1] n.+2 + S_[l.+1] n.+2 <= S_[a.-1] n.+2 + S_[c.+3] n.+2. rewrite addnC (_ : l.+1 = 1 + c.+2 + a.-2); last first. by rewrite /c a1E add1n !addSnnS !prednK ?subnK // -a1E ltnW. rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F7n : S_[1] n.+1 + S_[l] n.+1 <= S_[a.-1] n.+1 + S_[c.+2] n.+1. rewrite addnC (_ : l = 1 + c.+1 + a.-2); last first. by rewrite /c a1E add1n subSS !addSnnS !prednK ?subnK // -ltnS -a1E ltnW. rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). have cm1_gt0 : 0 < c.-1 by rewrite -subn1 ltn_subRL addn0. have F8n1 : S_[1] n.+2 + S_[c.+3] n.+2 <= S_[c.-1] n.+2 + S_[5] n.+2. rewrite addnC (_ : c.+3 = 1 + 4 + c.-2); last first. by rewrite add1n 2!addSnnS !prednK. rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F8n : S_[1] n.+1 + S_[c.+2] n.+1 <= S_[c.-1] n.+1 + S_[4] n.+1. rewrite addnC (_ : c.+2 = 1 + 3 + c.-2); last first. by rewrite add1n 2!addSnnS !prednK. rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). have F9 : S_[5] n.+2 <= S_[4] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha. have F10 : S_[4] n.+1 <= S_[3] n + (α_[1] n).*2. by apply: dsum_alphaL_alpha. have F11 : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S. have F12 := leq_dsum_alpha_2l_1 n.+1. have F13n1 := dsum_alphaL_S 1 n.+1. have F13n := dsum_alphaL_S 1 n. move: P4 P5 P6 P8 => P4 P5 P6 P8. rewrite -(leq_add2r x2S); applyr P4. rewrite -(leq_add2r y2S); applyr P5. rewrite -(leq_add2r (x3S + y3S)); applyr P6. rewrite -(leq_add2r (x5S + y5S)); applyr P8. applyl y5Sy2SE; applyl y3Sx5SE; applyl x2Sx3SE. rewrite [2 * (S_[_.-2] _)]mul2n -addnn {1}F1. rewrite [2 * (S_[_.-2] _)]mul2n -addnn {1}F2. rewrite [2 * (S_[3] _)]mul2n -addnn {1}F3. gsimpl. rewrite {}F4_a {}F4_c. applyr F4an; applyr F4an1; applyr F4cn; applyr F4cn1. applyl F5. rewrite -ltnS -!addSn -!addnA [X in _ <= X]addnC !addnA -ltnS -!addSn. rewrite -{}F6n -{}F6n1. rewrite -(leq_add2r (S_[1] n.+2)); applyl F7n1. rewrite -(leq_add2r (S_[1] n.+1)); applyl F7n; gsimpl. rewrite -(leq_add2r (S_[1] n.+2)); applyl F8n1. rewrite -(leq_add2r (S_[1] n.+1)); applyl F8n; gsimpl. applyl F9. rewrite -leq_double in F10; applyl F10. rewrite -(leq_add2r 2). changel (6 * S_[1] n + 4 * α_[1] n.+1 + (α_[1] n).*2 + (α_[1] n).*2 + ((S_[3] n).+1).*2). rewrite -{}F11. applyr F12. by rewrite F13n1 F13n; gsimpl. rewrite !ltnS leqn0 => /eqP bE0. have a1E : a1 = a by rewrite -(subnK aLa1) -/b bE0. pose u3 := [ffun i : 'I_5 => if i == 0 :> nat then sam1 else if i == 1 :> nat then tam1 else if i == 2 :> nat then ↓[u (inord a)] else if i == 3 :> nat then sa1 else ta1]. have cH6 (k : 'I_5) : 0 < k < 4 -> codom (u3 k) \subset [:: pa1; a[p2, pa1S] k]. move=> /andP[k_gt0 k_lt3]. rewrite !ffunE eqn_leq leqNgt k_gt0 /=. case: eqP => [->/=|/eqP kD1]. by rewrite /pa1S !apegS apeg0 codom_apeg. case: eqP =>[->/=|/eqP kD2]. apply: codom_liftr; rewrite codom_subC. have /cH : 0 < (inord a : 'I_l.+2) < l.+1. by rewrite inordK // a_gt0 /= -a1E. by rewrite inordK // /pa1 a1E. have ->/= : k = 3 :> nat. by case: (k : nat) k_lt3 k_gt0 kD1 kD2 => // [] [|[|[|]]]. by rewrite /pa1S !(apegS, apeg0) codom_apeg. have P6 : (S_[4] n.+1).*2 <= (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove + `d[↓[u (inord a)], sa1]_smove + `d[sa1, ta1]_smove) + sp sam1 4 p2 + sp ta1 4 p2. apply: (leq_trans (IH _ _ _ _ _ _ cH6)); rewrite /pa1S /pa1 //. - by rewrite eq_sym. - by rewrite eq_sym. - by rewrite apegS apeg_eqC. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /= ?a1E. - by apply: eq_bigr => i _; rewrite !ffunE /=. by apply: eq_bigr => i _; rewrite !ffunE /= a1E. set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6. have x2Sx3SE : x2S + x3S <= (S_[1] n).*2 + α_[maxn (3 * a).-2 4] n. by apply: sum_alpha_diffE; rewrite /pa. rewrite (maxn_idPl _) in x2Sx3SE; last first. by rewrite -subn2 ltn_subRL // (leq_mul2l 3 2). have y2Sy3SE : y2S + y3S <= (S_[1] n).*2 + α_[maxn (3 * c).-2 4] n. apply: sum_alpha_diffE => //; first by rewrite /pa1. by rewrite codom_subC. rewrite (maxn_idPl _) in y2Sy3SE; last first. by rewrite -subn2 ltn_subRL (leq_mul2l 3 2). rewrite (_ : sd u = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a1 <= i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first. pose f i := `d[u (inord i), u (inord i.+1)]_smove. by rewrite /sd -!(big_mkord xpredT f) a1E -!big_cat_nat. rewrite -{}P1 -{P3}P2. rewrite (_ : sd u1 = \sum_(i < (3 * a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove + `d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove); last first. pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f) . rewrite -{1}(subnK (_ : 1 < 3 * a)) //; last first. by rewrite -[a]prednK // mulnS. rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _). rewrite ffunE (_ : (3 * a).-2 = (3 * (a.-1)).+1); last first. by rewrite -{1}[a]prednK // mulnS. rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK. rewrite mod3E /= eqxx. rewrite ffunE inordK; last first. by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW. by rewrite mod3E /= eqxx. rewrite ffunE (_ : (3 * a).-2 = (3 * (a.-1)).+1); last first. by rewrite -{1}[a]prednK // mulnS. rewrite inordK; last first. by rewrite -{2}[a]prednK // mulnS. rewrite mod3E /= eqxx. rewrite ffunE inordK; last first. by rewrite -{2}[a]prednK // mulnS. by rewrite -[(_ * _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK. rewrite [X in _ <= _ + (_ + X) + _ + _](_ : _ = `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove + \sum_(i < (3 * c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove); last first. pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f) . rewrite -{1}(subnK (_ : 1 < 3 * c)) //; last first. by rewrite -[c]prednK // mulnS. rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA; congr (_ + _ + _). - rewrite !ffunE !inordK ?addn0 //=. by rewrite ltnS muln_gt0. - rewrite !ffunE !inordK //=. by rewrite ltnW // ltnS (leq_mul2l 3 1 c). by rewrite ltnS muln_gt0. by rewrite big_mkord. set z1S := \sum_(_ < _) _ in P4; set z2S := \sum_(_ < _) _ in P5. rewrite -/z1S -/z2S. rewrite a1E -/y1S. changer (a.*2 + c.*2 + (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove + `d[↓[u (inord a)], sa1]_smove + `d[sa1, ta1]_smove) + x1S + y1S + z1S + z2S). set d1 := `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _; rewrite -/d1 in P6. have F1 := dsum_alphaL_S (3 * a).-2 n. have F2 := dsum_alphaL_S (3 * c).-2 n. have F3 := dsum_alphaL_S 4 n. have F4_a : 2 * a = 2 + a.-1 + a.-1. by rewrite mul2n -{1}[a]prednK // -addnn addnS. have F4_c : 2 * c = 2 + c.-1 + c.-1. by rewrite mul2n -{1}[c]prednK // -addnn addnS. have F4 i k : 0 < i -> S_[i.-1] k.+1 <= S_[(3 *i).-2] k + i.-1. move=> i_gt0; apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[i]prednK // mulnS addSn add2n /=. have F4an := F4 a n a_gt0. have F4an1 := F4 a n.+1 a_gt0. have F4cn := F4 c n (c_gt0). have F4cn1 := F4 c n.+1 (c_gt0). have l_gt1 : 1 < l. by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add. have F5 := SH l_gt1. have am1_gt0 : 0 < a.-1 by rewrite -subn1 ltn_subRL addn0. have F6n1 : S_[1] n.+2 + S_[l.+1] n.+2 <= S_[a.-1] n.+2 + S_[c.+2] n.+2. rewrite addnC (_ : l.+1 = 1 + c.+1 + a.-2); last first. by rewrite /c add1n 2!addSnnS !prednK ?a1E ?subnK. rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F6n : S_[1] n.+1 + S_[l] n.+1 <= S_[a.-1] n.+1 + S_[c.+1] n.+1. rewrite addnC (_ : l = 1 + c + a.-2); last first. rewrite /c add1n a1E -{1}[a]prednK // subSS. by rewrite !addSnnS !prednK // subnK // -ltnS prednK. rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). have cm1_gt0 : 0 < c.-1 by rewrite -subn1 ltn_subRL addn0. have F7n1 : S_[1] n.+2 + S_[c.+2] n.+2 <= S_[c.-1] n.+2 + S_[4] n.+2. rewrite addnC (_ : c.+2 = 1 + 3 + c.-2); last first. by rewrite add1n 2!addSnnS !prednK. rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F7n : S_[1] n.+1 + S_[c.+1] n.+1 <= S_[c.-1] n.+1 + S_[3] n.+1. rewrite addnC (_ : c.+1 = 1 + 2 + c.-2); last first. by rewrite add1n 2!addSnnS !prednK. rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). have F8 : S_[4] n.+2 <= S_[3] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha n.+1 (isT : 1 < 3). have F9 : S_[3] n.+1 <= S_[4] n.+1 by case: (concave_dsum_alphaL_l n.+1). have F10n1 := dsum_alphaL_S 1 n.+1. have F10n := dsum_alphaL_S 1 n. have F11 := bound_alphaL 2 n. have F12 := alphaL_1_2 n. move: P4 P5 P6 => P4 P5 P6. rewrite -(leq_add2r x2S); applyr P4. rewrite -(leq_add2r y2S); applyr P5. rewrite -(leq_add2r (x3S + y3S)); applyr P6. applyl x2Sx3SE; applyl y2Sy3SE; gsimpl. rewrite [2 * (S_[_.-2] _)]mul2n -addnn {1}F1. rewrite [2 * (S_[_.-2] _)]mul2n -addnn {1}F2. gsimpl. rewrite {}F4_a {}F4_c. applyr F4an1; applyr F4an; applyr F4cn1; applyr F4cn. applyl F5. rewrite -(leq_add2r (S_[c.+2] n.+2)); applyr F6n1. rewrite -(leq_add2r (S_[c.+1] n.+1)); applyr F6n; gsimpl. rewrite -(leq_add2r (S_[1] n.+2)); applyl F7n1. rewrite -(leq_add2r (S_[1] n.+1)); applyl F7n. applyl F8; gsimpl. changel ((α_[1] n.+1).*2 + (S_[1] n).*2 + (S_[1] n).*2 + (α_[1] n.+1).*2 + (S_[3] n.+1).*2). changer (4 + S_[1] n.+2 + S_[1] n.+1 + S_[1] n.+2 + S_[1] n.+1 + (S_[4] n.+1).*2). apply: leq_add; last by rewrite leq_double. rewrite F10n1 F10n; gsimpl. by rewrite -leq_double in F12; applyl F12; gsimpl. rewrite negb_and -!leqNgt => acH. have aLc : a <= c by []. have aE1 : a = 1. case/orP: acH; case: (a) aLc a_gt0 => // [] [|n1] //. by case: (c) => // [] []. have leq_S4 k : 5 * S_[1] k.+1 + S_[1] k.+2 <= 6 * S_[4] k + 9. have F3 : 4 * S_[3] k + 2 * S_[6] k <= 6 * S_[4] k. rewrite -{1}[4]/(2 * 2) -mulnA -mulnDr -{2}[6]/(2 * 3) -mulnA. rewrite leq_mul2l /= -(leq_add2r (S_[5] k)). changel (S_[6] k + S_[3] k + (S_[5] k + S_[3] k)). changer (S_[5] k + S_[4] k + (S_[4] k + S_[4] k)). by apply: leq_add; apply: concaveEk1 3 _ _ (concave_dsum_alphaL_l k). applyr F3. have F3k : S_[1] k.+1 <= S_[3] k + 1 by apply: dsum_alpha3l. have F3k1 : S_[2] k.+1 <= S_[6] k + 2 by apply: dsum_alpha3l. rewrite -leq_double in F3k1; applyr F3k1. rewrite -2!leq_double in F3k; applyr F3k; gsimpl. by have F4 := leq_dsum_alpha_2l_1 k.+1; applyr F4. move: c_gt0; rewrite leq_eqVlt eq_sym => /orP[/eqP cE1|c_gt1]. move : P1 P2 P3 => P1 P2 P3. have l_gt0 : 0 < l by rewrite -ltnS l1E aE1 cE1 addn1. have a1El : a1 = l. by rewrite -(subKn (_ : a1 <= l.+1)) 1?ltnW // -/c cE1 subSS subn0. have [b_gt1|b_lt2]:= leqP 2 b. rewrite (_ : sd u = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a <= i < a1) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a1 <= i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first. pose f i := `d[u (inord i), u (inord i.+1)]_smove. rewrite /sd -!(big_mkord xpredT f). by rewrite -!big_cat_nat //= ltnW. rewrite !sum_beta_S // KH1 eqxx addn0 KH2 eqxx addn0. apply: leq_trans (leq_add (leq_add (leq_add (leq_add (leqnn _) P3) (leqnn _)) (leqnn _)) (leqnn _)); rewrite -{P3}P1 -{}P2. set x2S := sd u2; set x0S := sd u1. pose u3 := [ffun i : 'I_b.+1 => ↓[u (inord (a + i))]]. rewrite (_ : \sum_(_ <= _ < _) _ = \sum_(i < b) `d[u3 (inord i), u3 (inord i.+1)]_smove); last first. rewrite -{1}[a]add0n big_addn -/b big_mkord. apply: eq_bigr => i _. by rewrite !ffunE addnC !inordK ?(addnS, ltnS) // ltnW. pose paS := a[p1, p3] a.+1. have cH3 (k : 'I_b.+1) : 0 < k < b -> codom (u3 k) \subset [:: p2; a[pa, paS] k]. move=> /andP[k_gt0 k_ltb]. have akLl : a + k < l.+1. rewrite ltnS (leq_trans _ a1Ll) //. by rewrite -(subnK aLa1) addnC leq_add2r ltnW. rewrite !ffunE. have /H : 0 < (inord (a + k) : 'I_l.+2) < l.+1. rewrite inordK; first by rewrite addn_gt0 a_gt0. by rewrite ltnS ltnW. rewrite ffunE inordK //; last by rewrite ltnS ltnW. by rewrite /paS apegS -apegD [k + _]addnC. pose pa1 := a[p1, p3] a1. have P3 : (S_[b] n.+1).*2 <= \sum_(i < b) `d[↓[u (inord (a + i))], ↓[u (inord (a + i).+1)]]_smove + sp ↓[u (inord a)] b pa + sp ↓[u (inord a1)] b pa1. apply: leq_trans (IH _ _ _ _ _ _ cH3) (leq_add (leq_add _ _) _); rewrite /pa /paS // 1?eq_sym //. - by rewrite apegS apeg_eqC eq_sym. - apply: leq_sum => i; rewrite !ffunE !inordK ?addnS //. by rewrite ltnS. by rewrite ltnS ltnW. - by apply: leq_sum => i _; rewrite !ffunE addn0. apply: leq_sum => i _; rewrite !ffunE /= [a + b]addnC subnK //. by rewrite apegS -apegD subnK. set x1S := \sum_(_ < _) _ in P3; set y2S := sp _ _ _ in P3. set y3S := sp _ _ _ in P3. rewrite [\sum_(_ < _) _](_ : _ = x1S); last first. by apply: eq_bigr => i; rewrite !ffunE !inordK ?addnS // ltnS // ltnW. set y0S := \sum_(_ < _) _ ; set y5S := \sum_(_ < _) _. have cH1 (k : 'I_(3 * a).+1) : 0 < k < 3 * a -> codom (u1 k) \subset [:: p3; a[p1, p2] k]. move=> /andP[k_gt0 k_ltb]. rewrite {2}aE1 muln1 in k_ltb. rewrite ffunE !modn_small // !divn_small // inord_eq0 //. rewrite [in 3 * a.-1]aE1 /=. case: (k : nat) k_gt0 k_ltb => //= [] [|[|]] //= _ _. rewrite !(apegS, apeg0). by have := sam1C; rewrite /pa aE1 apegS apeg0. by rewrite !(apegS, apeg0) codom_subC. have P1 : (S_[3 * a] n.+1).*2 <= x0S + sp ↓[u ord0] 3 p1 + sp ↓[u (inord a)] 3 p2. apply: leq_trans (IH _ _ _ _ _ _ cH1) (leq_add (leq_add _ _) _); rewrite // 1?eq_sym //. by apply: leq_sum => i _; rewrite ffunE /= inord_eq0 // aE1 muln1. by apply: leq_sum => i _; rewrite ffunE /= mod3E /= div3E // aE1 muln1. have {}P1 := leq_trans P1 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). rewrite -/y0S in P1; set y1S := sp _ _ _ in P1. rewrite aE1 muln1 in P1. have y1Sy2SE : y1S + y2S <= (S_[1] n).*2 + α_[maxn 3 b] n. apply: sum_alpha_diffE => //; first by rewrite /pa // eq_sym. apply: codom_liftr. have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK. by rewrite /pa aE1 inordK. have cH2 (k : 'I_(3 * c).+1) : 0 < k < 3 * c -> codom (u2 k) \subset [:: a[p1, p3] a1; a[p2, a[p1, p3] a1.+1] k]. move=> /andP[k_gt0 k_ltb]. rewrite {2}cE1 muln1 in k_ltb. rewrite ffunE !modn_small // !divn_small // addn0. case: (k : nat) k_gt0 k_ltb => //= [] [|[|]] //= _ _. by rewrite !apegS apeg0 codom_apeg. by rewrite !(apegS, apeg0) codom_subC. have P2 : (S_[3 * c] n.+1).*2 <= x2S + sp ↓[u (inord a1)] 3 p2 + sp ↓[u ord_max] 3 (a[p3, p1] l). apply: leq_trans (IH _ _ _ _ _ _ cH2) (leq_add (leq_add _ _) _); rewrite // 1?eq_sym //. - by rewrite apegS apeg_eqC eq_sym. - by apply: leq_sum => i _; rewrite ffunE /= addn0 cE1 muln1. apply: leq_sum => i _; rewrite ffunE /= mod3E /= div3E // cE1 muln1. rewrite a1El addn1 (_ : inord _ = ord_max) ?apegS //. by apply/val_eqP; rewrite /= inordK. have {}P2 := leq_trans P2 (leq_add (leqnn _) (leq_sum_beta _ _)). rewrite -/y5S in P2; set y4S := sp _ _ _ in P2. have y3Sy4SE : y3S + y4S <= (S_[1] n).*2 + α_[maxn b 3] n. apply: sum_alpha_diffE; rewrite /pa /pa1 //. apply: codom_liftr; rewrite codom_subC. have /cH : 0 < (inord l : 'I_l.+2) < l.+1 by rewrite inordK // l_gt0 /=. by rewrite a1El inordK. have Eb1 : l = b.+1. by have := l1E; rewrite aE1 cE1 addn1 => [] []. rewrite Eb1. have F1b := dsum_alphaL_S b n. have F1n31 : (S_[3] n.+1).+1 = S_[1] n.+2. by rewrite dsum_alpha3_S. have F1n1 := dsum_alphaL_S 1 n. have F1n2 := dsum_alphaL_S 1 n.+1. have b_gt0 : 0 < b by apply: leq_trans b_gt1. have F2n1 : S_[b.+2] n.+2 <= S_[b.+1] n.+1 + (α_[1] n.+1).*2. by rewrite dsum_alphaL_alpha . have F2n : S_[b.+1] n.+1 <= S_[b] n + (α_[1] n).*2. by rewrite dsum_alphaL_alpha. have F3n : S_[4] n.+2 <= S_[3] n.+1 + (α_[1] n.+1).*2. by rewrite dsum_alphaL_alpha. have F4n := alphaL_3E n. have F5 := leq_dsum_alpha_2l_1 n.+1. move: P1 P2 P3 => P1 P2 P3. rewrite -(leq_add2r y1S); applyr P1. rewrite -(leq_add2r y4S); applyr P2. rewrite -(leq_add2r (y2S + y3S)); applyr P3. applyl y3Sy4SE; applyl y1Sy2SE; gsimpl. rewrite maxnC aE1 cE1 !muln1. changel ((S_[b.+2] n.+2 + (S_[1] n).*2 + α_[maxn 3 b] n).*2). changer (((S_[3] n.+1).+1.*2 + S_[b] n.+1).*2). rewrite leq_double. move: b_gt1; rewrite leq_eqVlt => /orP[/eqP<-|b_gt2]; last first. rewrite (maxn_idPr _) //. rewrite F1b addnA leq_add2r F1n31 F1n2 F1n1. by applyr F2n; applyr F2n1; gsimpl. rewrite (maxn_idPl _) //. applyl F3n; gsimpl. rewrite -ltnS -![in X in _ <= X]addSn !{}F1n31 {}F4n; gsimpl. rewrite F1n2; gsimpl. have [n_gt3 |] := leqP 4 n; last first. by case: n => [|[|[|[|n1]]]]; rewrite // !(alphaS_small, alpha_small). rewrite -leq_double; applyr F5. rewrite F1n2 F1n1; gsimpl. by have F := alpha_4_3 (n_gt3); applyr F. move: b_lt2; rewrite leq_eqVlt => /orP[/eqP [] bE1 | b_lt1]. pose u1l := [ffun i => if (i : 'I_5) == 0 :> nat then ↓[u ord0] else if i == 1 :> nat then sam1 else if i == 2 :> nat then tam1 else if i == 3 :> nat then ↓[u (inord 1)] else ↓[u (inord 2)]]. have a1E2 : a1 = 2. by move: (cE1); rewrite /c l1E aE1 bE1 cE1; case: (a1) => // [] [|[|]]. have P1l1 : a.*2 + sd u1l <= \sum_(i < a1) `d[u (inord i), u (inord i.+1)]_smove. rewrite /sd a1E2 !big_ord_recr /= !big_ord0 !add0n {1}aE1. rewrite !ffunE /= !inordK ?aE1 //= add2n -2!addSn leq_add //; last first. by apply/gdist_cunlift/shanoi_connect. rewrite (inord_eq0 _ (_ : 0 = 0)) //. rewrite (_ : ord0 = inord a.-1); last first. by apply/val_eqP; rewrite /= inordK aE1. by rewrite -[in inord 1]aE1 duam1ua1E /= addnA addn0. have cH1 (k : 'I_5) : 0 < k < 4 -> codom (u1l k) \subset [:: p3; a[p1, p2] k]. case: k => [] [|[|[|[|]]]] //= iH _; rewrite !ffunE !(apegS, apeg0). - by have := sam1C; rewrite /pa aE1. - by rewrite codom_subC. apply: codom_liftr; rewrite codom_subC. have /cH: 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK. by rewrite inordK. have lE2 : l = 2 by move: l1E; rewrite aE1 bE1 cE1 => [] []. have {cH1}P4 : (S_[4] n.+1).*2 <= sd u1l + sp ↓[u ord0] 4 p1 + sp ↓[u (inord a1)] 4 p1. apply: leq_trans (IH _ _ _ _ _ _ cH1) _ => //. by rewrite eq_sym. repeat apply: leq_add => //; apply: leq_sum => i /= _; rewrite !ffunE //. by rewrite a1El -[in inord 2]lE2. have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). set x1S := sd _ in P4. set y1S := \sum_(_ < _) _ in P4; set y2S := sp _ _ _ in P4. have cH2 (k : 'I_(3 * c).+1) : 0 < k < 3 * c -> codom (u2 k) \subset [:: a[p1, p3] a1; a[p2, a[p1, p3] a1.+1] k]. move=> /andP[k_gt0 k_ltb]. rewrite {2}cE1 muln1 in k_ltb. rewrite ffunE !modn_small // !divn_small // addn0. case: (k : nat) k_gt0 k_ltb => //= [] [|[|]] //= _ _. by rewrite a1E2. by rewrite codom_subC. have P5 : (S_[3 * c] n.+1).*2 <= sd u2 + sp ↓[u (inord a1)] 3 p2 + sp ↓[u ord_max] 3 (a[p3, p1] l). apply: leq_trans (IH _ _ _ _ _ _ cH2) (leq_add (leq_add _ _) _); rewrite // 1?eq_sym //. - by rewrite a1E2 eq_sym. - by apply: leq_sum => i _; rewrite ffunE /= addn0 cE1 muln1. apply: leq_sum => i _; rewrite ffunE /= mod3E /= div3E // cE1 muln1. rewrite a1El addn1 (_ : inord _ = ord_max) ?apegS //. by apply/val_eqP; rewrite /= inordK. have {}P5 := leq_trans P5 (leq_add (leqnn _) (leq_sum_beta _ _)). rewrite // {1}[in 3 *c]cE1 muln1 in P5. set x2S := sd _ in P5. set y3S := sp _ _ _ in P5; set y4S := \sum_(_ < _) _ in P5. rewrite /sd -(big_mkord xpredT (fun i => `d[u (inord i), u (inord i.+1)]_smove)). rewrite (big_cat_nat _ _ _ (_ : 0 <= a1)) //=; last by apply: ltnW. rewrite big_mkord -!addnA. apply: leq_trans (leq_add P1l1 (leqnn _)); rewrite -/x1S. rewrite -{P1l1}P2 -/x2S {1}lE2 !sum_beta_S //. rewrite KH1 KH2 !eqxx !addn0 aE1 -/y1S -/y4S. have y2Sy3SE : y2S + y3S <= (S_[1] n).*2 + α_[4] n. apply: sum_alpha_diffE => //. apply: codom_liftr; rewrite codom_subC. have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1 by rewrite inordK // a1E2 lE2. by rewrite inordK // a1E2. rewrite {1}aE1 -[1.*2]/2 in P1. rewrite {1}cE1 -[1.*2]/2. have F1n4 := dsum_alphaL_S 4 n. have F1n3 : (S_[3] n.+2).+1 = S_[1] n.+3. by rewrite -dsum_alpha3_S. have F1n13 : (S_[3] n.+1).+1 = S_[1] n.+2. by rewrite -dsum_alpha3_S. move: P4 P5 => P4 P5. rewrite -(leq_add2r y2S); applyr P4. rewrite -(leq_add2r y3S); applyr P5. applyl y2Sy3SE. rewrite [in X in _ <= X]mul2n -addnn. rewrite {1}F1n4; gsimpl. rewrite -(leq_add2r 2). changel (((S_[3] n.+2).+1).*2 + (S_[1] n).*2). changer (4 + S_[4] n + S_[4] n.+1 + ((S_[3] n.+1).+1).*2). rewrite {}F1n3 {}F1n13. case : n => [|[|[|[|n1]]]]; try by rewrite !alphaS_small. set m1 := n1.+3. rewrite -(leq_add2r (S_[1] m1.+2).*2). rewrite -[_ <= _](leq_mul2l 6). have F := leq_S4 m1.+1; applyr F. have F := leq_S4 m1.+2; applyr F; gsimpl. have F3n3 := dsum_alphaL_S 1 m1.+3. have F3n2 := dsum_alphaL_S 1 m1.+2. have F3n1 := dsum_alphaL_S 1 m1.+1. rewrite !(F3n3, F3n2, F3n1); gsimpl. have F4m1 : 12 * α_[1] m1.+3 <= 16 * α_[1] m1.+2. rewrite -[12]/(4 * 3) -mulnA. rewrite -[16]/(4 * 4) -mulnA leq_mul2l /=. by rewrite alpha_4_3. apply: leq_trans (leq_trans _ F4m1) _; first by rewrite leq_mul2r orbT. gsimpl. have F4m2 : 9 * α_[1] m1.+2 <= 12 * α_[1] m1.+1. rewrite -[12]/(3 * 4) -mulnA. rewrite -[9]/(3 * 3) -mulnA leq_mul2l /=. by rewrite alpha_4_3. by applyr F4m2; gsimpl. have bE0 : b = 0 by case: (b) b_lt1 => //. have lE1 : l = 1 by have := l1E; rewrite aE1 bE0 cE1 => [] []. have a1E1 : a1 = 1 by rewrite a1El. rewrite (_ : a[p3, p1] l = a[p2, p1] l); last by rewrite lE1. apply: (@case2 _ IH) => //. - by rewrite (_ : a[p1, p3] _ = a[p1, p3] 1). - move=> k hK; rewrite {3}lE1 in hK. have -> : k = inord 1. apply/val_eqP; rewrite /= inordK //. by case: (k : nat) hK => [] // [|]. rewrite inordK //= !(apegS, apeg0) //= codom_subC. have := cH (inord 1). rewrite inordK // !(apegS, apeg0). by apply. - by rewrite KH2 lE1. move=> k. have [->|[->|->]] // : k = ord0 \/ k = (inord 1) \/ k = (inord 2). - move: k; rewrite lE1. case => [] []; first by left; apply: val_inj => /=. case. by right; left; apply: val_inj; rewrite /= inordK. case => //. by right; right; apply: val_inj; rewrite /= inordK. by rewrite -[in inord 1]aE1 uaLEp2 aE1 inordK. rewrite {1}(_ : inord 2 = ord_max); last first. by apply/val_eqP; rewrite /= lE1 inordK. by rewrite KH2 lE1 /= inordK. pose u2r := [ffun i : 'I_(3 * c).-2.+1 => u2 (inord i.+2)]. pose pa1 := a[p1, p3] a1. pose pa1S := a[p1, p3] a1.+1. have cH8 (k : 'I_(3 * c).-2.+1) : 0 < k < (3 * c).-2 -> codom (u2r k) \subset [:: p2; a[pa1, pa1S] k]. move=> /andP[k_gt0 k3L3a]. have k2L3c : k.+2 < (3 * c). by have := k3L3a; rewrite -{2}subn2 ltn_subRL add2n. rewrite !ffunE inordK ?ltnS 1?ltnW //. case: eqP => [km3E0 /= |/eqP km3D0]. have k3_gt0 : 0 < k.+2 %/ 3. case: (k: nat) k_gt0 km3E0 => // [] //= k1 _ _. by rewrite (divnMDl 1 k1 (_ : 0 < 3)). have a1k3Ll1 : a1 + k.+2 %/ 3 < l.+1. move: k2L3c. rewrite {1}(divn_eq k.+2 3) km3E0 addn0 mulnC ltn_mul2l /= => k2L3c. rewrite -(subnK (_ : a1 <= l.+1)) ?(leq_trans a1Ll) //. by rewrite addnC ltn_add2r -/c. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first. by rewrite /pa1S !addnS !apegS -apegD addnC. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first. rewrite apegO oddD {1}(divn_eq k.+2 3) !oddD oddM andbT -oddD. by rewrite km3E0 addn0 -oddD -apegO. have /H : 0 < (inord (a1 + k.+2 %/ 3) : 'I_l.+2) < l.+1. rewrite inordK; first by rewrite addn_gt0 a1_gt0. by rewrite ltnS ltnW. by rewrite ffunE inordK // ltnS ltnW. case: eqP => [km3E1|/eqP km3D1]. rewrite eqn_leq ltnNge /=. have a1La1k : a1 < a1 + k.+2 %/3. by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0. have a1k3Ll : a1 + k.+2 %/ 3 < l.+1. move: (ltnW k2L3c). rewrite {1}(divn_eq k.+2 3) km3E1 addn1 mulnC ltn_mul2l /=. rewrite -(subnK (_ : a1 <= l.+1)) ?(leq_trans a1Ll) //. by rewrite addnC ltn_add2r -/c. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first. by rewrite /pa1S !addnS !apegS -apegD addnC. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3).+1) ; last first. rewrite apegS apegO {1}(divn_eq k.+2 3) !oddD oddM andbT. by rewrite km3E1 addbT addbN -oddD -oddS -apegO apegS. case: (sitiHb (a1 + k.+2 %/ 3)) => // [| siH _ _]; first by rewrite a1La1k. by move: siH; rewrite a1Max // ltnS ltnW. have km3E2 : k.+2 %% 3 = 2. by case: (_ %% _) (ltn_mod k.+2 3) km3D0 km3D1 => // [] [|[|]]. rewrite ifN; last by case: (k : nat) k_gt0. have a1La1k : a1 < a1 + k.+2 %/3. by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0. have a1k3Ll : a1 + k.+2 %/ 3 < l.+1. have: k.+2 %/ 3 * 3 < 3 * c. rewrite ltnW //. move: (ltnW k2L3c). by rewrite {1}(divn_eq k.+2 3) km3E2 addn2. rewrite mulnC ltn_mul2l /=. rewrite -(subnK (_ : a1 <= l.+1)) ?(leq_trans a1Ll) //. by rewrite addnC ltn_add2r -/c. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first. by rewrite !addnS /pa1S !apegS -apegD addnC. rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first. rewrite apegO {1}(divn_eq k.+2 3) !oddD oddM andbT. by rewrite km3E2 addbF -oddD -apegO. rewrite codom_subC. case: (sitiHb (a1 + k.+2 %/ 3)) => // [| _ tiH _]; first by rewrite a1La1k. by move: tiH; rewrite a1Max // a1La1k ltnS ltnW. have c_gt0 : 0 < c by rewrite ltnW. have P8 : (S_[(3 * c).-2] n.+1).*2 <= \sum_(i < (3 * c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove + sp ta1 (3 * c).-2 pa1 + sp ↓[u ord_max] (3 * c).-2 (a[p3, p1] l). apply: leq_trans (IH _ _ _ _ _ _ cH8) _; rewrite /pa1 /pa1S {cH8}//. - by rewrite apegS apeg_eqC. - by rewrite eq_sym. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - apply: eq_bigr => i _. by rewrite ![u2r _]ffunE !inordK // ltnS // ltnW. - apply: eq_bigr => i _; congr ((_ != _) * _). rewrite !ffunE /= !inordK //=. by rewrite (leq_trans (_ : 2 < (3 * 1).+1)) // ltnS leq_mul2l ltnW. apply: eq_bigr => i _; congr ((_ != _) * _). rewrite !ffunE /= !prednK ?muln_gt0 //=; last first. by rewrite -subn1 ltn_subRL addn0 (leq_trans (_ : _ < 3 * 1)) // leq_mul2l. rewrite inordK // mod3E /= div3E addnC subnK; last first. by apply: (leq_trans a1Ll). by rewrite ffunE; congr (u _ _ ); apply/val_eqP; rewrite /= inordK. rewrite /pa1 /pa1S -[RHS]apegS -(subnK (_ : a1 <= l.+1)) // -/c. rewrite apegS -apegD apegO -subn2 oddD oddB //. by rewrite oddM /= addbF -oddD -apegO. by rewrite (leq_trans (_ : _ < 3 * 1)) // leq_mul2l //. by rewrite ltnW. rewrite {cH8}//. have l_gt0 : 0 < l. by rewrite -ltnS l1E aE1 add1n addSn ltnS addn_gt0 c_gt0 orbT. have c3m2_gt1 : 1 < (3 * c).-2. by rewrite -subn2 ltn_subRL -[2 +1]/(3 * 1) ltn_mul2l. have {}P8 := leq_trans P8 (leq_add (leq_add (leqnn _) (leqnn _)) (leq_sum_beta _ _)). set y7S := sp _ _ _ in P8; set y8S := \sum_(_ < n.+1) _ in P8. rewrite !sum_beta_S // KH1 KH2 !eqxx !addn0 -/y8S. rewrite (_ : sd u = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a <= i < a1) `d[u (inord i), u (inord i.+1)]_smove + \sum_(a1 <= i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first. rewrite /sd -[X in _ = X + _ + _](big_mkord xpredT (fun i => `d[u (inord i), u (inord i.+1)]_smove)). by rewrite -!big_cat_nat ?big_mkord //= ltnW. rewrite -{}P1 -{}P2. move: P3 => P3. rewrite -2!addnA. apply: leq_trans (leq_add (leq_add (leqnn _) P3) (leqnn _)); rewrite {P3}//. have du2E : `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove = \sum_(i < 2) `d[u2 (inord i), u2 (inord i.+1)]_smove. rewrite !big_ord_recr /= big_ord0 !ffunE !inordK //= ?addn0 //. by rewrite ltnW // ltnS (leq_mul2l 3 1). by rewrite ltnS muln_gt0. rewrite (_ : sd u2 = (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) + \sum_(i < (3 * c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove); last first. rewrite /sd du2E. rewrite -!(big_mkord xpredT (fun i => `d[u2 (inord i), u2 (inord i.+1)]_smove)). rewrite -!(big_mkord xpredT (fun i => `d[u2 (inord i.+2), u2 (inord i.+3)]_smove)). rewrite[X in _ = _ + X] (eq_bigr (fun i => `d[u2 (inord (i + 2)), u2 (inord (i + 2).+1)]_smove)); last by move=> i_; rewrite !addn2. rewrite -subn2. have <- := big_addn _ _ _ xpredT (fun i => `d[u2 (inord i), u2 (inord i.+1)]_smove). rewrite -big_cat_nat //. by rewrite ltnW // (leq_mul2l 3 1). set x3S := \sum_(_ < _) _ in P8; rewrite -/x3S. have [|b_gt0] := leqP b 0; last first. have cH1 (k : 'I_(3 * a).+1) : 0 < k < 3 * a -> codom (u1 k) \subset [:: p3; a[p1, p2] k]. move=> /andP[k_gt0 k_ltb]. rewrite {2}aE1 muln1 in k_ltb. rewrite ffunE !modn_small // !divn_small // inord_eq0 //. rewrite [in 3 * a.-1]aE1 /=. case: (k : nat) k_gt0 k_ltb => //= [] [|[|]] //= _ _. rewrite apegS apeg0. by have := sam1C; rewrite /pa aE1. by rewrite codom_subC. set x0S := sd u1. have P4 : (S_[3 * a] n.+1).*2 <= x0S + sp ↓[u ord0] 3 p1 + sp ↓[u (inord a)] 3 p2. apply: leq_trans (IH _ _ _ _ _ _ cH1) (leq_add (leq_add _ _) _); rewrite // 1?eq_sym //. by apply: leq_sum => i _; rewrite ffunE /= inord_eq0 // aE1 muln1. by apply: leq_sum => i _; rewrite ffunE /= mod3E /= div3E // aE1 muln1. have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). set y0S := \sum_(_ < _) _ in P4; set y1S := sp _ _ _ in P4. have [b_gt1|b_le2] := leqP 2 b. pose u3 := [ffun i => ↓[u (inord ((i : 'I_b.+1) + a))]]. pose paS := a[p1, p3] a.+1. have cH6 (k : 'I_b.+1) : 0 < k < b -> codom (u3 k) \subset [:: p2; a[pa, paS] k]. move=> /andP[k_gt0 kLb]. have kBound : 0 < k + a < l.+1. rewrite (leq_trans a_gt0) ?leq_addl //=. move: kLb; rewrite /b ltn_subRL addnC => /leq_trans-> //. by rewrite ltnW. rewrite ffunE codom_liftr //. have := @cH (inord (k + a)). rewrite /pa /paS apegS -apegD /= !inordK //; last first. by rewrite ltnW // ltnS; case/andP: kBound. by apply. have {cH6}P6 : (S_[b] n.+1).*2 <= sd u3 + sp (u3 ord0) b pa + sp (u3 ord_max) b (a[pa, paS] b). apply: IH cH6 => //; try by rewrite /pa /paS // eq_sym. by rewrite /paS apegS apeg_eqC. set x1S := \sum_(_ <= _ < _) _. rewrite !ffunE (_ : sd u3 = x1S) in P6; last first. rewrite /x1S -[a]add0n big_addn -/b big_mkord. by apply: eq_bigr => i _; rewrite !ffunE !inordK ?ltnS // ltnW. rewrite add0n subnK // in P6. set y2S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6. have aLl : a <= l by apply: leq_trans aLa1 _. have y1Sy2SE : y1S + y2S <= (S_[1] n).*2 + α_[maxn 3 b] n. apply: sum_alpha_diffE => //; first by rewrite /pa eq_sym. apply/codom_liftr. have /cH : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite inordK // a_gt0. by rewrite inordK // aE1 /=. pose u5 := [ffun i : 'I_3 => if i == 0 :> nat then ↓[u (inord a1)] else if i == 1 :> nat then sa1 else ta1]. have cH7 (k : 'I_3) : 0 < k < 2 -> codom (u5 k) \subset [:: p1; a[p2, p3] k]. move=> /andP[k_gt0 k_lt2]. rewrite !ffunE. by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 => // [] [|]. have P7 : (S_[2] n.+1).*2 <= (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) + sp ↓[u (inord a1)] 2 p2 + sp ta1 2 p2. apply: (leq_trans (IH _ _ _ _ _ _ cH7)) => //. by rewrite eq_sym. repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP. - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=. - by apply: eq_bigr => i _; rewrite !ffunE. by apply: eq_bigr => i _; rewrite !ffunE. set x2S := (`d[_, _]_ _ + `d[_, _]_ _); rewrite -/x2S in P7. set y4S := sp _ _ _ in P7; set y5S := sp _ _ _ in P7. have y3Sy4SE : y3S + y4S <= (S_[1] n).*2 + α_[maxn b 2] n. apply: sum_alpha_diffE => //. by rewrite /paS apegS -apegD apeg_neq // eq_sym. apply: codom_liftr; rewrite codom_subC. have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1. by rewrite inordK ?a1_gt0 // ltnS (leq_trans a1Ll). rewrite inordK ?ltnS ?(leq_trans a1Ll) //. by rewrite /paS apegS -apegD subnK. rewrite (maxn_idPl _) // in y3Sy4SE. have y5Sy7SE : y5S + y7S <= (S_[1] n).*2 + α_[maxn 2 (3 * c).-2] n. by apply: sum_alpha_diffE => //; first by rewrite /pa1 eq_sym. rewrite (maxn_idPr _) // in y5Sy7SE. rewrite -/y0S. move: P4 P6 P7 P8 => P4 P6 P7 P8. rewrite -(leq_add2r y1S); applyr P4. rewrite -(leq_add2r (y2S + y3S)); applyr P6. rewrite -(leq_add2r (y4S + y5S)); applyr P7. rewrite -(leq_add2r y7S); applyr P8. applyl y5Sy7SE; applyl y3Sy4SE; applyl y1Sy2SE. rewrite aE1 !muln1. have F1 := dsum_alphaL_S (3 * c).-2 n. rewrite [X in _ <= _ + X]mul2n -addnn -ltnS ![in X in _ <= X]addnA -![in X in _ <= X]addnS {2}F1 {F1}//. gsimpl. have F2 i k : 0 < i -> S_[i.-1] k.+1 <= S_[(3 *i).-2] k + i.-1. move=> i_gt0; apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[i]prednK // mulnS addSn add2n /=. have F2n := F2 c n c_gt0. have F2n1 := F2 c n.+1 c_gt0. have F3 : c = c.-1.+1 by rewrite prednK. rewrite {}[in 2 * c]F3. gsimpl. applyr F2n; applyr F2n1; rewrite {F2}//. have l_gt1 : 1 < l. by rewrite -ltnS l1E aE1 add1n addSn ltnS (leq_trans b_gt1) // leq_addr. have F4 := SH l_gt1; applyl F4. have cB1_gt0 : 0 < c.-1 by rewrite -ltnS prednK. have F5 : S_[l.+1] n.+2 + S_[1] n.+2 <= S_[c.-1] n.+2 + S_[b.+3] n.+2. rewrite [X in _ <= X]addnC. rewrite (_ : l.+1 = 1 + c.-2 + b.+2); last first. by rewrite l1E aE1 !add1n -addSnnS !prednK // addnC. rewrite (_ : c.-1 = 1 + c.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F6 : S_[l] n.+1 + S_[1] n.+1 <= S_[c.-1] n.+1 + S_[b.+2] n.+1. rewrite [X in _ <= X]addnC. rewrite (_ : l = 1 + c.-2 + b.+1); last first. rewrite -[l]/(l.+1.-1) l1E aE1. by rewrite !add1n -addSnnS !prednK // addnC addnS. rewrite (_ : c.-1 = 1 + c.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). rewrite -(leq_add2r (S_[b.+2] n.+1)); applyr F6. rewrite -(leq_add2r (S_[b.+3] n.+2)); applyr F5; gsimpl. have [b_gt2|b_le3] := leqP 3 b. have F7 := dsum_alphaL_S b n; rewrite {}F7; gsimpl. have F8 : S_[b.+3] n.+2 <= S_[b.+2] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha. applyl F8. have F9 : S_[b.+1] n.+1 <= S_[b] n + (α_[1] n).*2. by apply: dsum_alphaL_alpha. rewrite -leq_double in F9. rewrite -(leq_add2r (4 * α_[1] n)); applyr F9. have F10 : S_[1] n.+1 + S_[b.+2] n.+1 <= S_[b.+1] n.+1 + S_[2] n.+1. rewrite addnC -[b.+2]/(1 + 1 + b). by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). rewrite -leq_double in F10; applyr F10. rewrite -2!ltnS [in X in _ <= X]mul2n -![in X in _ <= X]addSn -doubleS. have F11 := dsum_alpha3_S n.+1; rewrite -F11. have F12 := dsum_alphaL_S 1 n.+1; rewrite F12. have F13 := dsum_alphaL_S 1 n; rewrite !F13; gsimpl. by have F14 := alphaL_1_2 n; applyl F14; gsimpl. have bE2 : b = 2. by case: (b) b_gt1 b_le3 => // [] [|[|]]. rewrite bE2. rewrite ![in X in _ <= X]mul2n -!addnn. have F1 := dsum_alphaL_S 2 n; rewrite {1}F1. have F2 := dsum_alphaL_S 3 n; rewrite {1}F2. have F3 : S_[5] n.+2 <= S_[4] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha. rewrite -[3 + 2]/5 -[2 + 2]/4; applyl F3. have F4 : S_[4] n.+1 <= S_[3] n + (α_[1] n).*2. by apply: dsum_alphaL_alpha. rewrite -leq_double in F4; applyl F4; gsimpl. rewrite -ltnS. have F5 := dsum_alpha3_S n.+1. rewrite -![in X in _ <= X]addSn -F5. have F6 := dsum_alpha3_S n. rewrite addnAC -!addnS -F6. rewrite -leq_double. have F7 := leq_dsum_alpha_2l_1 n.+1. have F8 := leq_dsum_alpha_2l_1 n. rewrite -[_ <= _]orFb -(leq_mul2l 3) in F7. applyr F7; applyr F8; gsimpl. have F9 := dsum_alphaL_S 1 n.+1. have F10 := dsum_alphaL_S 1 n. rewrite !(F9, F10); gsimpl. by have F11 := alphaL_1_2 n; applyl F11; gsimpl. have bE1 : b = 1. by case: (b) b_gt0 b_le2 => // [] [|]. have a1E2 : a1 = 2. by move: bE1; rewrite /b aE1; case: (a1) => // [] [|[]]. pose u3 := [ffun i : 'I_4 => if i == 0 :> nat then ↓[u (inord a)] else if i == 1 :> nat then ↓[u (inord a1)] else if i == 2 :> nat then sa1 else ta1]. set x1S := \sum_(_ <= _ < _) _. set d1 := `d[_, _]_ _ + `d[_, _]_ _. rewrite -/y0S. changer (a.*2 + x0S + c.*2 + x3S + y0S + y8S + (x1S + d1)). have -> : x1S + d1 = \sum_(i < 3) `d[u3 (inord i), u3 (inord i.+1)]_smove. rewrite /x1S aE1 a1E2 big_nat1 /d1 !big_ord_recr big_ord0 /=. by rewrite !ffunE !inordK //= aE1 a1E2 add0n !addnA. have l_gt2 : 2 < l by rewrite -ltnS l1E aE1 bE1 !add1n. set x6S := \sum_(_ < 3) _. have cH6 (k : 'I_4) : 0 < k < 3 -> codom (u3 k) \subset [:: pa1; a[pa1S, p2] k]. move=> /andP[k_gt0 k_lt3]. rewrite !ffunE eqn_leq leqNgt k_gt0 /=. case: eqP => [->/=|/eqP kD1]. apply: codom_liftr; rewrite codom_subC. have /cH : 0 < (inord a1 : 'I_l.+2 ) < l.+1. by rewrite inordK a1E2 // (leq_trans l_gt2). by rewrite inordK // a1E2 (leq_trans l_gt2) // ltnW. have -> : k = 2 :> nat. by case: (k : nat) k_gt0 k_lt3 kD1 => // [] [|[]]. by have := sa1C; rewrite eqxx /pa1 /pa1S !(apegS, apeg0) codom_apeg. have P6 : (S_[3] n.+1).*2 <= x6S + sp (u3 ord0) 3 pa1S + sp (u3 ord_max) 3 p2. apply: IH cH6; rewrite /pa1S /pa1 //. by rewrite a1E2 eq_sym. rewrite !ffunE /= in P6. set y2S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6. have y1Sy2SE : y1S + y2S <= (S_[1] n).*2 + α_[3] n. apply: sum_alpha_diffE => //; first by rewrite eq_sym /pa1S a1E2. have /H : 0 < (inord a : 'I_l.+2) < l.+1; first by rewrite inordK // aE1. by rewrite ffunE inordK // /pa1S /= aE1 a1E2. have lEc : l = c.+1 by rewrite -[l]/l.+1.-1 l1E aE1 bE1. rewrite lEc. have y3Sy7SE : y3S + y7S <= (S_[1] n).*2 + α_[maxn 3 (3 * c).-2] n. by apply: sum_alpha_diffE => //; first by rewrite /pa1 a1E2 eq_sym. rewrite (maxn_idPr _) in y3Sy7SE; last first. by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2). move: P4 P6 P8 => P4 P6 P8. rewrite -(leq_add2r y1S); applyr P4. rewrite -(leq_add2r (y2S + y3S)); applyr P6. rewrite -(leq_add2r y7S); applyr P8. rewrite aE1 !muln1. applyl y1Sy2SE; applyl y3Sy7SE. rewrite ![in X in _ <= X]mul2n -!addnn. have F1 := dsum_alphaL_S 3 n; rewrite {1}F1. have F2 := dsum_alphaL_S (3 * c).-2 n; rewrite {1}F2; gsimpl. have F4 k : S_[c.-1] k.+1 <= S_[(3 *c).-2] k + c.-1. apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[c]prednK // mulnS addSn add2n /=. have F4n := F4 n. have F4n1 := F4 n.+1. have F5 := prednK c_gt0. rewrite -{}[in 2 * c]F5. applyr F4n1; applyr F4n. have l_gt1 : 1 < l by rewrite lEc. have F6 : (S_[c.+2] n.+2).*2 <= S_[c.+2] n.+2 + S_[c.+1] n.+1 + (α_[1] n.+1).*2. by have := (SH l_gt1); rewrite lEc. applyl F6. have F7 : S_[c.+2] n.+2 + S_[1] n.+2 <= S_[c.-1] n.+2 + S_[4] n.+2. rewrite (_ : c.+2 = 1 + 3 + c.-2); last first. by rewrite !addSn add0n !prednK ?addn2 // -ltnS prednK. rewrite {2}(_ : c.-1 = 1 + c.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F8 : S_[c.+1] n.+1 + S_[1] n.+1 <= S_[c.-1] n.+1 + S_[3] n.+1. rewrite (_ : c.+1 = 1 + 2 + c.-2); last first. by rewrite !addSn add0n !prednK ?addn2 // -ltnS prednK. rewrite {2}(_ : c.-1 = 1 + c.-2); last first. by rewrite add1n prednK // -ltnS prednK. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). rewrite -(leq_add2r (S_[1] n.+2 + S_[1] n.+1)); applyl F7; applyl F8; gsimpl. have F9 : S_[4] n.+2 <= S_[3] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha. applyl F9. have F10 := dsum_alpha3_S n. have F11 := dsum_alpha3_S n.+1. gsimpl. rewrite -ltnS -![in X in _ <= X]addSn -{}F11. rewrite -ltnS -3![in X in _ <= X]addSn -[in X in _ <= X]addnS -{}F10. have F12 := dsum_alphaL_S 1 n.+1. have F13 := dsum_alphaL_S 1 n. rewrite F12 F13; gsimpl. have F14 := alphaL_1_2 n; rewrite -leq_double in F14. by applyl F14; gsimpl. rewrite leqn0 => /eqP bE0. have a1Ea : a1 = a by rewrite -(subnK aLa1) -/b bE0. rewrite big_geq ?a1Ea // addn0. have lEc : l = c by rewrite -[l]/(l.+1.-1) l1E aE1 bE0. rewrite {1}lEc. set d1 := `d[_, _]_ _ + `d[_, _]_ _. set x0S := sd _; set y0S := \sum_(_ < _) _. changer (a.*2 + c.*2 + x3S + y0S + y8S + (x0S + d1)). pose u3 := [ffun i : 'I_6 => if i == 0 :> nat then ↓[u ord0] else if i == 1 :> nat then sam1 else if i == 2 :> nat then tam1 else if i == 3 :> nat then ↓[u (inord a1)] else if i == 4 :> nat then sa1 else ta1]. have -> : x0S + d1 = sd u3. rewrite /x0S /d1 /sd. rewrite -(big_mkord xpredT (fun i => `d[u1 (inord i), u1 (inord i.+1)]_ _)). rewrite {1}aE1 !(big_nat1, big_nat_recr) // !big_ord_recr big_ord0 /= ?inordK //= !ffunE ?inordK ?a1Ea ?aE1 //=. by rewrite add0n !addnA inord_eq0. have cH4 (k : 'I_6) : 0 < k < 5 -> codom (u3 k) \subset [:: p3; a[p1, p2] k]. case: k => [] [|[|[|[|[]]]]] //= iH _; rewrite !ffunE !(apegS, apeg0). - by have := sam1C; rewrite /pa aE1. - by rewrite codom_subC. - rewrite a1Ea aE1. - have /H : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite !inordK. by rewrite ffunE inordK // codom_subC. by rewrite codom_subC. have P4 : (S_[5] n.+1).*2 <= sd u3 + sp ↓[u ord0] 5 p1 + sp ta1 5 p2. apply: leq_trans (IH _ _ _ _ _ _ cH4) _ => //; first by rewrite eq_sym. by apply: leq_add; rewrite !ffunE. have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). rewrite -/y0S in P4; set y1S := sp _ _ _ in P4. set x1S := sd _ in P4; rewrite -/x1S. have y1Sy7SE : y1S + y7S <= (S_[1] n).*2 + α_[maxn 5 (3 * c).-2] n. apply: sum_alpha_diffE => //; first by rewrite /pa1 eq_sym. move: P4 P8 => P4 P8. rewrite -(leq_add2r y1S); applyr P4. rewrite -(leq_add2r y7S); applyr P8. rewrite aE1 muln1. applyl y1Sy7SE. have leq_S5 k : 2 * S_[1] k.+1 + S_[1] k.+2 <= 3 * S_[5] k + 6. have F8 : S_[3] k + 2 * S_[6] k <= 3 * S_[5] k. rewrite -(leq_add2r (S_[4] k)). changel (S_[6] k + S_[3] k + (S_[6] k + S_[4] k)). changer (S_[4] k + S_[5] k + (S_[5] k + S_[5] k)). apply: leq_add. by apply: concaveEk1 3 2 1 (concave_dsum_alphaL_l _). by apply: concaveEk1 4 1 1 (concave_dsum_alphaL_l _). apply: leq_trans (leq_add F8 (leqnn _)). have F3k : S_[1] k.+1 <= S_[3] k + 1 by apply: dsum_alpha3l. have F3k1 : S_[2] k.+1 <= S_[6] k + 2 by apply: dsum_alpha3l. rewrite -leq_double in F3k1; applyr F3k1; applyr F3k; gsimpl. have F3k2 := leq_dsum_alpha_2l_1 k.+1. by applyr F3k2. have [c_gt2|c_lt3] := leqP 3 c. rewrite (maxn_idPr _); last by rewrite -subn2 ltn_subRL (ltn_mul2l 3 2). have F1 k : S_[c.-1] k.+1 <= S_[(3 *c).-2] k + c.-1. apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[c]prednK // mulnS addSn add2n /=. have F1n := F1 n. have F1n1 := F1 n.+1. have F2 := dsum_alphaL_S (3 * c).-2 n. rewrite [X in _ <= _ + X]mul2n -addnn {1}F2; gsimpl. have F3 : 2 * c = 2 + c.-1 + c.-1. by rewrite mul2n add2n prednK // addSnnS prednK // addnn. rewrite {}F3. applyr F1n; applyr F1n1. have F4 : S_[c.+1] n.+2 <= S_[c] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha. applyl F4. have F7n1 : S_[2] n.+2 + S_[c.+1] n.+2 <= S_[c.-1] n.+2 + S_[4] n.+2. rewrite addnC (_ : c.+1 = 2 + 2 + c.-2.-1); last first. by rewrite !addSn add0n !prednK // -ltnS prednK // -subn1 ltn_subRL //. rewrite {2}(_ : c.-1 = 2 + c.-1.-2); last first. by rewrite !addSn add0n !prednK // -?subn2 -?subn1 ltn_subRL. by apply: concaveEk1 (concave_dsum_alphaL_l n.+2). have F7n : S_[2] n.+1 + S_[c] n.+1 <= S_[c.-1] n.+1 + S_[3] n.+1. rewrite addnC {1}(_ : c = 2 + 1 + c.-1.-2); last first. by rewrite !addSn add0n !prednK // -2!ltnS !prednK // -ltnS prednK. rewrite {2}(_ : c.-1 = 2 + c.-1.-2); last first. by rewrite !addSn add0n !prednK // -?subn2 -?subn1 ltn_subRL. by apply: concaveEk1 (concave_dsum_alphaL_l n.+1). rewrite -(leq_add2l (S_[2] n.+2 + S_[2] n.+1)); applyl F7n1; applyl F7n. gsimpl. have F8 := leq_S5 n.+1. have F9 : S_[4] n.+2 <= S_[3] n.+1 + (α_[1] n.+1).*2. by apply: dsum_alphaL_alpha. applyl F9. rewrite -[_ <= _](leq_mul2l 3). rewrite -leq_double in F8; applyr F8. have F10 := dsum_alpha3_S n.+1. rewrite -(leq_add2r 6). changel (12 * (α_[1] n.+1) + 6 * (S_[1] n) + 6 * (S_[3] n.+1).+1). rewrite -F10. rewrite -leq_double. have F11 := leq_dsum_alpha_2l_1 n.+2. rewrite -[_ <= _](leq_mul2l 3) in F11. have F12 := leq_dsum_alpha_2l_1 n.+1. rewrite -[_ <= _](leq_mul2l 3) in F12. applyr F11; applyr F12; gsimpl. have F13 := dsum_alphaL_S 1 n.+2. have F14 := dsum_alphaL_S 1 n.+1. have F15 := dsum_alphaL_S 1 n. rewrite !(F13, F14, F15); gsimpl. have F16 := increasing_alphaL 1 n.+1. rewrite -[15]/(7 + 8) mulnDl [X in _ <= X]addnAC [X in _ <= X]addnC leq_add //. by rewrite leq_mul2l. case: (n) => [|[|[|[|n1]]]]; rewrite ?alpha_small //. have F17 : 3 * α_[1] n1.+1.+4 <= 4 * α_[1] n1.+4. by rewrite alpha_4_3. rewrite -[_ <= _]orFb -(leq_mul2l 8) mulnA in F17. rewrite -[_ <= _](leq_mul2l 3) mulnA. by apply: leq_trans F17 _; gsimpl. have cE2 : c = 2 by case: (c) c_gt1 c_lt3 => [|[|[|]]]. rewrite cE2 (maxn_idPl _) // add1n -[2 * 2]/4 -[(3 * 2).-2]/4 -[2 + 4]/6. rewrite [in X in _ <= X]mul2n -addnn. have F1 := dsum_alphaL_S 5 n; rewrite {1}F1. have F2 := dsum_alpha3_S n.+2. rewrite -2!ltnS mul2n -![in X in X <= _]addSn -doubleS -{}F2. have F3 := leq_S5 n. have F4 := leq_S5 n.+1. rewrite -[_ <= _](leq_mul2l 3); gsimpl. applyr F3; applyr F4. have F5 := leq_S4 n.+1; applyr F5. have F6 := dsum_alphaL_S 1 n.+2. have F7 := dsum_alphaL_S 1 n.+1. have F8 := dsum_alphaL_S 1 n. rewrite !(F6, F7, F8); gsimpl. have F10 := alphaL_1_2 n.+1. rewrite -[_ <= _]orFb -(leq_mul2l 4) in F10. applyl F10; gsimpl. case: (n) => [|[|[|[|n1]]]]; rewrite ?alpha_small //. have F9 : 3 * α_[1] n1.+1.+4 <= 4 * α_[1] n1.+4. by rewrite alpha_4_3. rewrite -[_ <= _]orFb -(leq_mul2l 4) in F9. rewrite -[_ <= _](leq_mul2l 3). by rewrite add1n; applyl F9; gsimpl. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)