proposition: Lemma case1 : (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. have apeg13D0 := apeg13D0; have apeg13D2 := apeg13D2. have il1E : inord l.+1 = ord_max :> 'I_l.+2 by apply/val_eqP; rewrite /= inordK. have iE : exists i, u (inord i) ord_max != a[p1, p3] i. by exists l.+1; rewrite apegS il1E. case: (@ex_minnP _ iE) => a aH aMin. 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 aLld1 : a <= l.+1 by apply: aMin; rewrite apegS il1E. have a_gt0 : 0 < a by case: (a) aH; rewrite // apeg0 -KH1 inord_eq0 //= eqxx. pose ai : 'I_l.+2 := inord a. have aiE : ai = a :> nat by rewrite inordK. pose b := l.+1 - a. pose bi : 'I_l.+2 := inord b. have biE : bi = b :> nat by rewrite inordK // /b ltn_subLR // leq_addl. have l_ggt0 : 0 < l by case: l l_gt0. have [/andP[a_gt1 aLlm1]|] := boolP (2 <= a <= l.-1). have aLl : a <= l by rewrite (leq_trans aLlm1) // -subn1 leq_subr. have b_gt1 : 1 < b by rewrite leq_subRL // addn2 ltnS -[l]prednK. have uaiLEp2 : u ai ldisk = p2. have /cH/subsetP/(_ (u ai ldisk) (codom_f _ _)) : 0 < ai < l.+1. by rewrite aiE (leq_trans _ a_gt1) //= ltnS (leq_trans aLl1) // ssrnat.leq_pred. by rewrite !inE aiE (negPf aH) orbF => /eqP. 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 => //. - by rewrite aMin1. - rewrite !aMin1 //; last by rewrite -[a]prednK. by rewrite apegS apeg_eqC. - by rewrite aMin1 1?eq_sym // -[a]prednK. - by rewrite aMin1. by rewrite aMin1 // -[a]prednK. pose sam1 : configuration 4 n.+1 := sgdist1 (a[p1, p3] a) (u (inord a.-1)) (u (inord a)). pose tam1 : configuration 4 n.+1 := sgdist2 (a[p1, p3] a) (u (inord a.-1)) (u (inord a)). have [sam1C tam1C duam1ua1E] : [/\ codom sam1 \subset [:: a[p1, p3] a; u (inord a) ldisk ], codom tam1 \subset [:: u (inord a.-1) ldisk; a[p1, p3] a] & `d[u (inord a.-1), u (inord a)]_smove = D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2]. apply: sgdistE => //. - by rewrite aMin1 ?prednK // -{2}[a]prednK //= apegS apeg_eqC. - by rewrite uaiLEp2 aMin1 ?prednK. - by rewrite uaiLEp2. - by rewrite aMin1 ?prednK. by rewrite uaiLEp2. have {}tam1C : codom tam1 \subset [:: p1; p3]. move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK. rewrite -subn1 apegO oddB //= [a[_, _]a]apegO; case: odd => //=. by rewrite codom_subC. pose u1 := [ffun i => if ((i : 'I_(3 * a).-2.+1) == 3 * a.-1 :>nat) then ↓[u (inord a.-1)] else if (i == (3 * a.-1).+1 :>nat) then sam1 else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))] else if (i %% 3) == 1 then si (i %/ 3) else ti (i %/ 3)]. have u10E : u1 ord0 = ↓[u ord0]. rewrite ffunE /= ifN ?inord_eq0 //. by rewrite neq_ltn muln_gt0 /= -ltnS prednK //= a_gt1. have uiME : u1 ord_max = sam1. rewrite ffunE /= eqn_leq leqNgt -{2}[a]prednK // mulnS. rewrite addSn add2n ltnS leqnn /=. by rewrite -{1}[a]prednK // mulnS eqxx. pose u2 := [ffun i : 'I_3 => if i == 0 :> nat then sam1 else if i == 1 :> nat then tam1 else ↓[u ai]]. pose u3 := [ffun i => ↓[u (inord ((i : 'I_b.+1) + a))]]. have P1 : a.*2 + sd u1 + sd u2 + sd u3 <= sd u. have G b1 : b1 = a -> \sum_(i < (3 * b1).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove = \sum_(i < (3 * a.-1)) `d[u1 (inord i), u1 (inord i.+1)]_smove + `d[↓[u (inord a.-1)], sam1]_smove. move=> b1Ea. have ta2E : (3 * b1).-2 = (3 * a.-1).+1. by rewrite b1Ea -{1}[a]prednK // mulnS. rewrite ta2E big_ord_recr /=; congr (_ + `d[_,_]_smove). by rewrite ffunE ifT// inordK // -{2}b1Ea ?ta2E. rewrite ffunE inordK; last by rewrite -{2}b1Ea ?ta2E. by rewrite eqn_leq ltnn /= eqxx. rewrite {}[sd u1]G //. have -> := @sum3E _ (fun i => `d[u1 (inord i), u1 (inord i.+1)]_smove). have -> : a.*2 = 2 + \sum_(i < a.-1) 2. rewrite sum_nat_const /= cardT size_enum_ord. by rewrite muln2 -(doubleD 1) add1n prednK. rewrite !addnA -[2 + _ + _]addnA -big_split /=. rewrite [2 + _]addnC -!addnA 2![X in _ + X <= _]addnA addnA. have -> : sd u = \sum_(i < a.-1) (`d[u (inord i), u (inord i.+1)]_smove) + `d[u (inord a.-1), u ai]_smove + \sum_(i < b) `d[u (inord (a +i)), u (inord (a + i.+1))]_smove. have F := big_mkord xpredT (fun i => `d[u (inord i), u (inord i.+1)]_smove). rewrite -{}[sd u]F. rewrite (big_cat_nat _ _ _ (_ : _ <= (a.-1).+1)) //=; last first. by rewrite prednK. rewrite big_mkord big_ord_recr /= prednK //. rewrite -{9}[a]add0n big_addn -/b big_mkord. congr (_ + _ + _). by apply: eq_bigr => i; rewrite addnC addnS. apply: leq_add; first apply: leq_add. - rewrite leq_eqVlt; apply/orP; left; apply/eqP. apply: eq_bigr => i _. have -> : u1 (inord (3 * i)) = ↓[u (inord i)]. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. by rewrite leq_mul2l /= ltnW. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_mul2l /= eqn_leq [_ <= i]leqNgt ltn_ord andbF. rewrite eqn_leq ltn_mul2l /= ltnNge [i <= _]ltnW // andbF. by rewrite mod3E eqxx mulKn. have -> : u1 (inord (3 * i).+1) = si i. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. by rewrite ltn_mul2l /=. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_leq [_ <= _.+1]leqNgt. rewrite (leq_trans (_ : (3 * i).+2 <= (3 * i.+1))) ?andbF //; last 2 first. - by rewrite mulnS addSn add2n. - by rewrite leq_mul2l /=. rewrite eqn_leq !ltnS [_ <= 3 * i]leq_mul2l. by rewrite [_ <= i]leqNgt ltn_ord andbF mod3E /= div3E. have -> : u1 (inord (3 * i).+2) = ti i. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. rewrite (leq_trans (_ : _ <= 3 * (i.+1))) //. by rewrite mulnS addSn add2n. by rewrite leq_mul2l /=. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_leq [_ <= _.+1]leqNgt. rewrite -[(3 * i).+3](mulnDr 3 1 i) leq_mul2l ltn_ord andbF. rewrite eqn_leq !ltnS [_ <= _.+1]leqNgt. rewrite (leq_trans (_ : (3 * i).+1 < 3 * (i.+1))) ?andbF //; last 2 first. - by rewrite mulnS addSn add2n. - by rewrite leq_mul2l /=. by rewrite mod3E /= div3E. have -> : u1 (inord (3 * i).+3) = ↓[u (inord i.+1)]. have -> : (3 * i).+3 = 3 * (i.+1) by rewrite mulnS addSn add2n. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. by rewrite leq_mul2l /=. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_mul2l /=; case: eqP => [->//|_]. rewrite eqn_leq [_ <= 3 * i.+1]leqNgt ltnS leq_mul2l /= ltn_ord andbF. by rewrite mod3E /= div3E. case: (sitiH i) => // _ _ ->. by rewrite add2n /= addnA addn0. - rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite /sd !big_ord_recr big_ord0 //= add0n !addnA. have -> : u2 (inord 0) = sam1 by rewrite ffunE /= inordK. have -> : u2 (inord 1) = tam1 by rewrite ffunE /= inordK. have -> : u2 (inord 2) = ↓[u ai] by rewrite ffunE /= inordK. by move: duam1ua1E; rewrite /= addn0 add2n !addnA !addSn. apply: leq_sum => i _. rewrite ffunE inordK; last by rewrite ltnS ltnW. rewrite ffunE inordK; last by rewrite ltnS. rewrite addSn [i + _]addnC addnS. by apply/gdist_cunlift/shanoi_connect. set x1P1 := sd _ in P1; set x2P1 := sd _ in P1. set x3P1 := sd _ in P1; set xP1 := sd _ in P1. rewrite -/xP1. have cH2 (k : 'I_(3 * a).-2.+1) : 0 < k < (3 * a).-2 -> codom (u1 k) \subset [:: p2; a[p1, p3] k]. move=> /andP[k_gt0 k_lt]. have kL3a1 : k <= (3 * a.-1). by rewrite -ltnS (leq_trans k_lt) // -{1}[a]prednK // mulnS. have kLa1 : k %/ 3 <= a.-1. by rewrite -(mulKn a.-1 (isT : 0 < 3)) leq_div2r. rewrite ffunE; case: eqP => [kH|/eqP kH]. rewrite kH apegMr //. have := @Hcodom(inord a.-1); rewrite inordK //. rewrite ffunE; apply. by rewrite -ltnS prednK // a_gt1. by rewrite prednK // (leq_trans aLld1). have k3La2 : k %/ 3 <= a.-2. rewrite -ltnS [a.-2.+1]prednK //; last first. by rewrite -subn1 ltn_subRL. rewrite ltn_divLR // [_ * 3]mulnC. by move: kL3a1 kH; case: ltngtP. rewrite eqn_leq [_ <= k]leqNgt (leq_trans k_lt) ?andbF //; last first. by rewrite -{1}[a]prednK // mulnS addSn add2n. have k3La : k %/ 3 <= a. by rewrite (leq_trans kLa1) // -subn1 leq_subr. case: eqP => k3mH. apply: codom_liftr. rewrite {2}(divn_eq k 3) k3mH addn0 [in a[_,_] _]mulnC apegMr //. have := @cH (inord (k %/3)); rewrite inordK; last first. by rewrite (leq_ltn_trans k3La). apply. rewrite (leq_ltn_trans k3La) ?ltnS //. move: k_gt0; rewrite andbT {1}(divn_eq k 3) k3mH addn0 muln_gt0. by case/andP. case: eqP => k3mH1. case: (sitiH ((k %/ 3))) => /=. by rewrite -[a.-1]prednK // -ltnS prednK. set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp. set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k. rewrite (divn_eq k 3) k3mH1 addn1 apegS mulnC apegMr //. by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La). have H2 : (k %/ 3).+1 < l.+2 by rewrite !ltnS (leq_trans k3La). rewrite -(@aMin1 i); last first. rewrite !inordK // -{2}[a]prednK // ltnS // -[a.-1]prednK // . by rewrite -subn1 subn_gt0. congr (u _ _). by apply/val_eqP; rewrite /= !inordK. rewrite codom_subC. case: (sitiH ((k %/ 3))) => /= [|_]. by rewrite -[a.-1]prednK // -ltnS prednK. set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp. set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k. have k3mH2 : k %% 3 = 2. have := ltn_mod k 3; move: k3mH k3mH1. by case: modn => // [] [|[]]. rewrite (divn_eq k 3) k3mH2 addn2 !apegS mulnC apegMr //. by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La). have H2 : (k %/ 3) < l.+2 by rewrite !ltnS (leq_trans k3La). rewrite -(@aMin1 i); last by rewrite !inordK // -{2}[a]prednK . congr (u _ _). by apply/val_eqP; rewrite /= !inordK. have {cH2}P2 := IH p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH2. have a3B2_gt1 : 1 < (3 * a).-2. rewrite -subn2 leq_subRL. by rewrite (leq_trans (_ : 4 <= 3 * 2)) // leq_mul2l. by rewrite (leq_trans (_ : 2 <= 3 * 2)) // leq_mul2l. rewrite u10E uiME apeg0 in P2. have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). pose pa := a[p1, p3] a; pose paS := a[p1, p3] a.+1. have cH3 (k : 'I_3) : 0 < k < 2 -> codom (u2 k) \subset [:: paS; a[p2, pa] k]. case: k => [] [|[|]] //= iH _. by rewrite /pa /paS !apegS apeg0 ffunE /= codom_apeg codom_subC. rewrite -/x1P1 in P2. have {cH3}P3 : (S_[2] n.+1).*2 <= sd u2 + sp (u2 ord0) 2 (a[p2, pa] 0) + sp (u2 ord_max) 2 (a[p2, pa] 2). apply: IH cH3 => //; try by rewrite /pa /paS // eq_sym. by rewrite /pa /paS apegS apeg_eqC eq_sym. rewrite !ffunE /= apeg0 -/x2P1 in P3. have cH4 (k : 'I_b.+1) : 0 < k < b -> codom (u3 k) \subset [:: p2; a[pa, paS] k]. rewrite /b . move=> /andP[k_gt0 kLb]. have kBound : 0 < k + a < l.+1. rewrite (leq_trans a_gt0) ?leq_addl //=. by move: kLb; rewrite /b ltn_subRL addnC. rewrite ffunE codom_liftr //. have := @cH (inord (k + a)). rewrite /pa /paS apegS inordK; first by rewrite -apegD; apply. by rewrite ltnW // ltnS; case/andP: kBound. have {cH4}P4 : (S_[b] n.+1).*2 <= sd u3 + sp (u3 ord0) b (a[pa, paS] 0) + sp (u3 ord_max) b (a[pa, paS] b). apply: IH cH4 => //; try by rewrite /pa /paS // eq_sym. by rewrite /pa /paS apegS apeg_eqC. have {}P4 := leq_trans P4 (leq_add (leqnn _) (leq_sum_beta _ _)). rewrite apeg0 /= (_ : a[_, _] b = a[p3, p1] l) in P4; last first. by rewrite /pa /paS apegS -apegD subnK ?apegS. rewrite !ffunE /= add0n -/ai in P4. rewrite -/x3P1 subnK // (_ : inord l.+1 = ord_max) in P4; last first. by apply/val_eqP; rewrite /= inordK. rewrite [X in _ <= _ + X + _]sum_beta_S //= KH1 eqxx addn0. set xS := \sum_(_ < _) _ in P2; rewrite -/xS. rewrite [X in _ <= _ + _ + X]sum_beta_S //= KH2 mul1n. set yS := \sum_(_ < _) _ in P4; rewrite -/yS. set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3. have x1Sy1SE : x1S + y1S <= (S_[1] n).*2 + α_[maxn (3 * a).-2 2] n. apply: sum_alpha_diffE => //. rewrite apeg32E //. by move: sam1C; rewrite -uiME uaiLEp2. rewrite (maxn_idPl _) // in x1Sy1SE. set x2S := sp _ _ _ in P3; set y2S := sp _ _ _ in P4. have x2y2SE : x2S + y2S <= (S_[1] n).*2 + α_[maxn 2 b] n. apply: sum_alpha_diffE => //; first by rewrite /pa eq_sym. have /Hcodom : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite inordK // a_gt0. by rewrite ffunE inordK. rewrite -addnn {1}dsum_alphaL_S in P2. rewrite -addnn {1}dsum_alphaL_S in P3. rewrite -addnn {1}dsum_alphaL_S. have F4 k : S_[a.-1] k.+1 <= S_[(3 *a).-2] k + a.-1. apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[a]prednK // mulnS addSn add2n /=. have F4n := F4 n. have {F4}F4n1 := F4 n.+1. have F5 k : S_[l.+1] k.+1 + S_[1] k.+1 + S_[b.+1] k.+1 <= S_[a.-1] k.+1 + S_[b.+2] k.+1 + S_[b] k + (α_[1] k).*2. have <- : a + b = l.+1 by rewrite addnC subnK. rewrite -[X in _ <= X]addnA (leq_add _ (dsum_alphaL_alpha k b_gt1)) //. have := concaveEk1 1 a.-2 b.+1 (concave_dsum_alphaL_l k.+1). rewrite add1n prednK; last by rewrite -subn1 ltn_subRL addn0. by rewrite -addSnnS prednK // add1n [X in _ <= X]addnC. have F5n := F5 n. have {F5}F5n1 := F5 n.+1. have F6 k : S_[b.+2] k + S_[1] k <= S_[b.+1] k + S_[2] k. by have := concaveEk1 1 1 b (concave_dsum_alphaL_l k). have F6n := F6 n.+1. have {F6}F6n1 := F6 n.+2. have F72 := dsum_alphaL_S 2 n.+1. have F721 := dsum_alphaL_S 2 n. have F711 := dsum_alphaL_S 1 n.+1. have F71 := dsum_alphaL_S 1 n. have F73 := dsum_alphaL_S b n. have F8 : α_[2] n.+1 <= α_[1] n.+2. have ->: α_[1] n.+2 = α_[3] n.+1 by rewrite alphaL_3E. by apply: increasing_alphaL_l. have F9 : α_[1] (n.+2) <= (α_[1] n).*2.+2. apply: leq_trans (leqnSn _). by apply: alphaL_4_5. gsimpl. applyr P1. rewrite -(leq_add2r x1S); applyr P2. rewrite -(leq_add2r (y1S + x2S)); applyr P3. rewrite -(leq_add2r y2S); applyr P4. applyl x2y2SE; applyl x1Sy1SE. rewrite -[in 2 * a](prednK a_gt0). applyr F4n; applyr F4n1; gsimpl. rewrite (maxn_idPr _) //. rewrite -(leq_add2r (S_[1] n.+1 + S_[b.+1] n.+1)); applyl F5n. rewrite -(leq_add2r (S_[1] n.+2 + S_[b.+1] n.+2)); applyl F5n1. gsimpl. rewrite -(leq_add2r (S_[1] n.+1)); applyl F6n; gsimpl. rewrite F71; gsimpl. rewrite !add1n {}F73; gsimpl. rewrite -(leq_add2r (S_[1] n.+2 + S_[2] n.+2)). applyl F6n1; gsimpl. rewrite {}F72 {}F721 {}F711 {}F71; gsimpl. applyl F8. by applyl F9; gsimpl. rewrite negb_and -leqNgt -ltnNge => oH. have [/andP[a_gt1 /eqP bE1]|] := boolP ((1 < a) && (b == 1)). have am1_gt0 : 0 < a.-1 by rewrite -subn1 subn_gt0. have lEa : l = a. have : a + b = l.+1 by rewrite addnC subnK //. by rewrite bE1 addn1 => [] []. have uaiLEp2 : u ai ldisk = p2. have /cH/subsetP/(_ (u ai ldisk) (codom_f _ _)) : 0 < ai < l.+1. by rewrite aiE a_gt0 lEa /=. by rewrite !inE aiE (negPf aH) orbF => /eqP. 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 => //. - by rewrite aMin1. - rewrite !aMin1 //; last by rewrite -[a]prednK. by rewrite apegS apeg_eqC. - by rewrite aMin1 1?eq_sym // -[a]prednK. - by rewrite aMin1. by rewrite aMin1 // -[a]prednK. 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 //. - by rewrite aMin1 ?prednK // -{2}[a]prednK //= apegS apeg_eqC. - by rewrite uaiLEp2 aMin1 // prednK. - by rewrite uaiLEp2. - by rewrite aMin1 // prednK. by rewrite uaiLEp2. 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 => if ((i : 'I_(3 * a).-2.+1) == 3 * a.-1 :>nat) then ↓[u (inord a.-1)] else if (i == (3 * a.-1).+1 :>nat) then sam1 else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))] else if (i %% 3) == 1 then si (i %/ 3) else ti (i %/ 3)]. have u10E : u1 ord0 = ↓[u ord0]. rewrite ffunE /= ifN ?inord_eq0 //. by rewrite neq_ltn muln_gt0 /= -ltnS prednK //= a_gt1. have uiME : u1 ord_max = sam1. rewrite ffunE /= eqn_leq leqNgt -{2}[a]prednK // mulnS. rewrite addSn add2n ltnS leqnn /=. by rewrite -{1}[a]prednK // mulnS eqxx. pose u2 := [ffun i : 'I_4 => if i == 0 :> nat then sam1 else if i == 1 :> nat then tam1 else if i == 2 :> nat then ↓[u ai] else ↓[u (inord (l.+1))]]. have P1 : a.*2 + sd u1 + sd u2 <= sd u. have G b1 : b1 = a -> \sum_(i < (3 * b1).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove = \sum_(i < (3 * a.-1)) `d[u1 (inord i), u1 (inord i.+1)]_smove + `d[↓[u (inord a.-1)], sam1]_smove. move=> b1Ea. have ta2E : (3 * b1).-2 = (3 * a.-1).+1. by rewrite b1Ea -{1}[a]prednK // mulnS. rewrite ta2E big_ord_recr /=; congr (_ + `d[_,_]_smove). by rewrite ffunE ifT// inordK // -{2}b1Ea ?ta2E. rewrite ffunE inordK; last by rewrite -{2}b1Ea ?ta2E. by rewrite eqn_leq ltnn /= eqxx. rewrite {}[sd u1]G //. have -> := @sum3E _ (fun i => `d[u1 (inord i), u1 (inord i.+1)]_smove). have -> : a.*2 = 2 + \sum_(i < a.-1) 2. rewrite sum_nat_const /= cardT size_enum_ord. by rewrite muln2 -(doubleD 1) add1n prednK. rewrite !addnA -[2 + _ + _]addnA -big_split /=. rewrite [sd u2]big_ord_recr /=. rewrite [u2 (inord 2)]ffunE inordK //=. rewrite [u2 (inord 3)]ffunE inordK //=. rewrite [2 + _]addnC -!addnA 2![X in _ + X <= _]addnA addnA. have -> : sd u = \sum_(i < a.-1) (`d[u (inord i), u (inord i.+1)]_smove) + `d[u (inord a.-1), u ai]_smove + `d[u ai, u (inord ai.+1)]_smove. rewrite -lEa (_ : ai = inord l); last first. by apply/val_eqP; rewrite /= aiE inordK // lEa. case: l l_gt0 u => //= l1 _ f. rewrite /sd 2!big_ord_recr //=; congr (_ + _ + `d[f _, f _]_smove). by apply/val_eqP; rewrite /= !inordK. apply: leq_add; first apply: leq_add. - rewrite leq_eqVlt; apply/orP; left; apply/eqP. apply: eq_bigr => i _. have -> : u1 (inord (3 * i)) = ↓[u (inord i)]. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. by rewrite leq_mul2l /= ltnW. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_mul2l /= eqn_leq [_ <= i]leqNgt ltn_ord andbF. rewrite eqn_leq ltn_mul2l /= ltnNge [i <= _]ltnW // andbF. by rewrite mod3E /= div3E. have -> : u1 (inord (3 * i).+1) = si i. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. by rewrite ltn_mul2l /=. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_leq [_ <= _.+1]leqNgt. rewrite (leq_trans (_ : (3 * i).+2 <= (3 * i.+1))) ?andbF //; last 2 first. - by rewrite mulnS addSn add2n. - by rewrite leq_mul2l /=. rewrite eqn_leq !ltnS [_ <= 3 * i]leq_mul2l. by rewrite [_ <= i]leqNgt ltn_ord andbF mod3E /= div3E. have -> : u1 (inord (3 * i).+2) = ti i. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. rewrite (leq_trans (_ : _ <= 3 * (i.+1))) //. by rewrite mulnS addSn add2n. by rewrite leq_mul2l /=. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_leq [_ <= _.+1]leqNgt. rewrite -[(3 * i).+3](mulnDr 3 1 i) leq_mul2l ltn_ord andbF. rewrite eqn_leq !ltnS [_ <= _.+1]leqNgt. rewrite (leq_trans (_ : (3 * i).+1 < 3 * (i.+1))) ?andbF //; last 2 first. - by rewrite mulnS addSn add2n. - by rewrite leq_mul2l /=. by rewrite mod3E /= div3E. have -> : u1 (inord (3 * i).+3) = ↓[u (inord i.+1)]. have -> : (3 * i).+3 = 3 * (i.+1) by rewrite mulnS addSn add2n. rewrite ffunE inordK; last first. rewrite ltnS (leq_trans (_ : _ <= 3 * (a.-1))) //. by rewrite leq_mul2l /=. by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW. rewrite eqn_mul2l /=; case: eqP => [->//|_]. rewrite eqn_leq [_ <= 3 * i.+1]leqNgt ltnS leq_mul2l /= ltn_ord andbF. by rewrite mod3E /= div3E. case: (sitiH i) => //= _ _. by rewrite !addnA addn0 add2n. - rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite !big_ord_recr big_ord0 //= add0n !addnA. have -> : u2 (inord 0) = sam1 by rewrite ffunE /= inordK. have -> : u2 (inord 1) = tam1 by rewrite ffunE /= inordK. have -> : u2 (inord 2) = ↓[u ai] by rewrite ffunE /= inordK. by move: duam1ua1E; rewrite /= addn0 add2n !addnA !addSn. rewrite (_ : inord l.+1 = inord ai.+1); last first. by apply/val_eqP; rewrite /= !inordK // lEa. by apply/gdist_cunlift/shanoi_connect. set x1P1 := sd _ in P1; set x2P1 := sd _ in P1. set xP1 := sd _ in P1; rewrite -/xP1. have cH2 (k : 'I_(3 * a).-2.+1) : 0 < k < (3 * a).-2 -> codom (u1 k) \subset [:: p2; a[p1, p3] k]. move=> /andP[k_gt0 k_lt]. have kL3a1 : k <= (3 * a.-1). by rewrite -ltnS (leq_trans k_lt) // -{1}[a]prednK // mulnS. have kLa1 : k %/ 3 <= a.-1. by rewrite -(mulKn a.-1 (isT : 0 < 3)) leq_div2r. rewrite ffunE; case: eqP => [kH|/eqP kH]. rewrite kH apegMr //. have := @Hcodom (inord a.-1); rewrite inordK //. rewrite ffunE; apply. by rewrite -ltnS prednK // a_gt1. by rewrite prednK // (leq_trans aLld1). have k3La2 : k %/ 3 <= a.-2. rewrite -ltnS [a.-2.+1]prednK //. rewrite ltn_divLR // [_ * 3]mulnC. by move: kL3a1 kH; case: ltngtP. rewrite eqn_leq [_ <= k]leqNgt (leq_trans k_lt) ?andbF //; last first. by rewrite -{1}[a]prednK // mulnS addSn add2n. have k3La : k %/ 3 <= a. by rewrite (leq_trans kLa1) // -subn1 leq_subr. case: eqP => k3mH. apply: codom_liftr. rewrite {2}(divn_eq k 3) k3mH addn0 [in a[_,_] _]mulnC apegMr //. have := @cH (inord (k %/3)); rewrite inordK; last first. by rewrite (leq_ltn_trans k3La). apply. rewrite (leq_ltn_trans k3La) ?ltnS ?lEa //. move: k_gt0; rewrite andbT {1}(divn_eq k 3) k3mH addn0 muln_gt0. by case/andP. case: eqP => k3mH1. case: (sitiH (k %/ 3)); first by rewrite -[a.-1]prednK. set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp. set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k. rewrite (divn_eq k 3) k3mH1 addn1 apegS mulnC apegMr //. by rewrite /i !inordK ?apegS //= !ltnS lEa. have H2 : (k %/ 3).+1 < l.+2 by rewrite !ltnS lEa (leq_trans k3La). rewrite -(@aMin1 i); last first. by rewrite !inordK // -{2}[a]prednK // ltnS // -[a.-1]prednK. congr (u _ _). by apply/val_eqP; rewrite /= !inordK. rewrite codom_subC. case: (sitiH (k %/ 3)) => [|_]; first by rewrite -[a.-1]prednK. set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp. set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k. have k3mH2 : k %% 3 = 2. have := ltn_mod k 3; move: k3mH k3mH1. by case: modn => // [] [|[]]. rewrite (divn_eq k 3) k3mH2 addn2 !apegS mulnC apegMr //. by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La). have H2 : (k %/ 3) < l.+2 by rewrite !ltnS (leq_trans k3La). rewrite -(@aMin1 i); last by rewrite !inordK // -{2}[a]prednK . congr (u _ _). by apply/val_eqP; rewrite /= !inordK. have {cH2}P2 := IH p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH2. have a3B2_gt1 : 1 < (3 * a).-2. rewrite -subn2 leq_subRL. by rewrite (leq_trans (_ : 4 <= 3 * 2)) // leq_mul2l. by rewrite (leq_trans (_ : 2 <= 3 * 2)) // leq_mul2l. rewrite u10E uiME apeg0 in P2. have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). rewrite -/x1P1 in P2. pose paS := a[p1, p3] a.+1. have cH3 (k : 'I_4) : 0 < k < 3 -> codom (u2 k) \subset [:: pa; a[p2, paS] k]. case: k => [] [|[|[|]]] //= iH _; rewrite ffunE /=. by have := tam1C; rewrite /pa /paS !(apegS, apeg0) codom_apeg. apply: codom_liftr. have /cH : 0 < ai < l.+1 by rewrite aiE a_gt0 // lEa /=. by rewrite /pa /paS !(apegS, apeg0) aiE codom_subC. have {cH3}P3 : (S_[3] n.+1).*2 <= sd u2 + sp (u2 ord0) 3 (a[p2, paS] 0) + sp (u2 ord_max) 3 (a[p2, paS] 3). apply: IH cH3 => //; try by rewrite /pa /paS // eq_sym. by rewrite /paS apegS apeg_eqC. have {}P3 := leq_trans P3 (leq_add (leqnn _) (leq_sum_beta _ _)). rewrite /pa /paS -lEa !(apegS, apeg0) in P3. rewrite !ffunE /= -/x2P1 (_ : inord l.+1 = ord_max) in P3; last first. by apply/val_eqP; rewrite /= inordK. rewrite [X in _ <= _ + X + _]sum_beta_S //= KH1 eqxx addn0. set xS := \sum_(_ < _) _ in P2; rewrite -/xS. rewrite [X in _ <= _ + _ + X]sum_beta_S //= KH2 mul1n. set yS := \sum_(i < _) _ in P3; rewrite -/yS. set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3. have x1Sy1SE : x1S + y1S <= (S_[1] n).*2 + α_[maxn (3 * a).-2 3] n. apply: sum_alpha_diffE => //. by move: sam1C; rewrite -uiME uaiLEp2 /pa apeg32E. rewrite (maxn_idPl _) // in x1Sy1SE; last first. by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2). rewrite -addnn {1}dsum_alphaL_S in P2. rewrite -addnn {1}dsum_alphaL_S. have F4 k : S_[a.-1] k.+1 <= S_[(3 *a).-2] k + a.-1. apply: leq_trans (dsum_alpha3l _ _) _. rewrite leq_add2r. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite -{2}[a]prednK // mulnS addSn add2n /=. have F4n := F4 n. have {F4}F4n1 := F4 n.+1. have F6 k : S_[a.+1] k + S_[1] k <= S_[a.-1] k + S_[3] k. have := concaveEk1 1 a.-2 2 (concave_dsum_alphaL_l k). by rewrite add1n addn2 !prednK // [_ + S_[3] _]addnC. have F6n := F6 n.+1. have {F6}F6n1 := F6 n.+2. have F72 := dsum_alphaL_S 3 n.+1. have F721 := dsum_alphaL_S 3 n. have F711 := dsum_alphaL_S 1 n.+1. have F71 := dsum_alphaL_S 1 n. have F8 : α_[1] n.+2 = α_[3] n.+1 by rewrite alphaL_3E. have F9 : α_[1] (n.+2) <= (α_[1] n).*2.+2. apply: leq_trans (leqnSn _). by apply: alphaL_4_5. gsimpl. applyr P1. rewrite -(leq_add2r x1S); applyr P2. rewrite -(leq_add2r y1S); applyr P3. applyl x1Sy1SE; gsimpl. rewrite -(leq_add2r (S_[a.-1] n.+1)) -[in 2 * a](prednK a_gt0). applyl F4n. rewrite -(leq_add2r (S_[a.-1] n.+2)); applyl F4n1. rewrite lEa; applyr F6n. rewrite -(leq_add2r (S_[1] n.+2 + S_[3] n.+2)); applyr F6n1. rewrite {}F72 {}F711 {}F71; gsimpl. rewrite !add1n -{}F8. by applyl F9; gsimpl. rewrite negb_and -leqNgt => o1H. have [/eqP aE1| aD1] := boolP (a == 1). have b_gt0 : 0 < b by rewrite /b aE1 subn1. have bE : b = l by rewrite /b aE1 subn1. move: b_gt0; rewrite leq_eqVlt => /orP[/eqP bE1 | b_gt1]; last first. have u1C : u (inord 1) ldisk = p2. move: aH; rewrite aE1 apegS apeg0. have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK. move=> /subsetP/(_ (u (inord 1) ldisk) (codom_f _ _)). by rewrite !inE => /orP[] /eqP-> //; rewrite !inordK // apegS apeg0 eqxx. pose s0 : configuration 4 n.+1 := sgdist1 p3 (u ord0) (u (inord 1)). pose t0 : configuration 4 n.+1 := sgdist2 p3 (u ord0) (u (inord 1)). have [s0C t0C ds0t0E] : [/\ codom s0 \subset [:: p3; u (inord 1) ldisk ], codom t0 \subset [:: u ord0 ldisk; p3] & `d[u ord0, u (inord 1)]_smove = D[[:: ↓[u ord0]; s0; t0; ↓[u (inord 1)]]].+2]. apply: sgdistE => //. - by rewrite /= KH1. - by rewrite KH1 u1C. - by rewrite u1C eq_sym. - by rewrite KH1. by rewrite u1C. pose u1 := [ffun i : 'I_4 => if i == 0 :> nat then ↓[u ord0] else if i == 1 :> nat then s0 else if i == 2 :> nat then t0 else ↓[u (inord 1)]]. pose u2 := [ffun i => ↓[u (inord ((i : 'I_b.+1) + 1))]]. have P1 : 2 + sd u1 + sd u2 <= sd u. have -> : sd u = `d[u ord0, u (inord 1)]_smove + \sum_(i < b) `d[u (inord (a +i)), u (inord (a + i.+1))]_smove. rewrite /sd big_ord_recl /= bE. congr (`d[u _,u _]_smove + _). by apply/val_eqP; rewrite /= inordK. apply: eq_bigr => i _. congr (`d[u _,u _]_smove); apply/val_eqP; rewrite aE1 /= inordK //=. by rewrite /bump add1n !ltnS ltnW. by rewrite /bump add1n !ltnS. apply: leq_add. rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite /sd !big_ord_recr /= big_ord0 add0n. rewrite !ffunE !inordK //= add2n. by rewrite ds0t0E /= addn0 !addnA. apply: leq_sum => i _. rewrite ffunE inordK; last by rewrite ltnS ltnW. rewrite ffunE inordK; last by rewrite ltnS. rewrite aE1 addSn [i + _]addnC addnS. by apply/gdist_cunlift/shanoi_connect. set x1P1 := sd _ in P1; set x2P1 := sd _ in P1. set xP1 := sd _ in P1; rewrite -/xP1. have cH2 (k : 'I_4) : 0 < k < 3 -> codom (u1 k) \subset [:: p3; a[p1, p2] k]. case: k => [] [|[|[|]]] //= iH _; rewrite ffunE /= !(apegS, apeg0). by have := s0C; rewrite u1C. by rewrite codom_subC -KH1. have {cH2}P2 : (S_[3] n.+1).*2 <= sd u1 + sp ↓[u (inord 0)] 3 (a[p1, p2] 0) + sp ↓[u (inord 1)] 3 (a[p1, p2] 3). apply: leq_trans (IH _ _ _ _ _ _ cH2) _ => //. by rewrite eq_sym. repeat apply: leq_add => //; rewrite leq_eqVlt; apply/orP; left; apply/eqP. by apply: eq_bigr => i _; rewrite !ffunE inord_eq0. by apply: eq_bigr => i _; rewrite !ffunE. have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)). rewrite -/x2P1 (inord_eq0) // -[in inord 1]aE1 !(apegS, apeg0) in P2. have cH3 (k : 'I_b.+1) : 0 < k < b -> codom (u2 k) \subset [:: p2; a[p3, p1] k]. rewrite [X in k < X]bE => /andP[k_gt0 kLb]. rewrite ffunE addn1; apply: codom_liftr. have := @cH (inord k.+1). rewrite inordK ?apegS //=; first by apply. by rewrite ltnS (leq_trans kLb). have {cH3}P3 : (S_[b] n.+1).*2 <= sd u2 + sp ↓[u (inord 1)] b p3 + sp ↓[u ord_max] b (a[p3, p1] b). apply: leq_trans (IH _ _ _ _ _ _ cH3) _ => //; try by rewrite eq_sym. repeat apply: leq_add => //; rewrite leq_eqVlt; apply/orP; left; apply/eqP; apply: eq_bigr => i _. by rewrite !ffunE. rewrite !ffunE /= addn1 bE; congr ((u _ _ != _) * _). by apply/val_eqP; rewrite /= inordK. have {}P3 := leq_trans P3 (leq_add (leqnn _) (leq_sum_beta _ _)). rewrite -/x2P1 (_ : a[p3, p1] b = a[p3, p1] l) in P3; last first. by rewrite bE. rewrite -[in inord 1]aE1 in P3. rewrite !sum_beta_S // KH1 eqxx mul0n addn0 KH2 mul1n. set xS := \sum_(i < _) _ in P2; rewrite -/xS. set yS := \sum_(i < _) _ in P3; rewrite -/yS. set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3. have x1Sy1SE : x1S + y1S <= (S_[1] n).*2 + α_[maxn 3 b] n. apply: sum_alpha_diffE => //. apply: codom_liftr. have /cH : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite aE1 inordK. by rewrite inordK aE1. rewrite -/x1P1 in P2. rewrite -addnn {1}dsum_alphaL_S -bE. gsimpl; applyr P1. rewrite -(leq_add2r x1S); applyr P2. rewrite -(leq_add2r y1S); applyr P3. applyl x1Sy1SE; gsimpl. move: b_gt1; rewrite leq_eqVlt => /orP[/eqP bE2|b_gt2]. rewrite -bE2 (maxn_idPl _) //. rewrite [S_[3] n.+2]dsum_alphaL_S; gsimpl. rewrite !alphaL_3E. have F := leq_dsum_alpha_2l_1 n.+1; applyr F. rewrite !dsum_alphaL_S; gsimpl. rewrite !add1n. by have F := alphaL_4_5 n; applyl F; gsimpl. rewrite (maxn_idPr _) //. changer (2 * (S_[3] (n.+1)).+1 + 2 * S_[b] (n.+1)). rewrite -dsum_alpha3_S. rewrite ![in X in _ <= 2 * X + _]dsum_alphaL_S; gsimpl. rewrite [in X in _ <= _ + X]mul2n -addnn. rewrite [in X in _ <= _ + (X + _)]dsum_alphaL_S; gsimpl. changer ((S_[b] n + (α_[1] n).*2) + (S_[b] n.+1 + (α_[1] n.+1).*2)). by apply: leq_add; apply: dsum_alphaL_alpha; apply: ltnW. have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK. move=> /subsetP /(_ (u (inord 1) ldisk) (codom_f _ _)). rewrite !inE inordK // apegS apeg0. have := aH; rewrite (_ : inord a = inord 1); last first. by apply/val_eqP; rewrite /= !inordK // aE1. rewrite aE1 apegS => /negPf->; rewrite orbF => /eqP u1LE. case: (@sgdistE _ p3 (u ord0) (u (inord 1))) => //. - by rewrite KH1. - by rewrite KH1 u1LE. - by rewrite u1LE eq_sym. - by rewrite KH1. by rewrite u1LE. set s0 := sgdist1 _ _ _; set t0 := sgdist2 _ _ _. move=> s0C t0C du0u1; rewrite /= !addnA addn0 in du0u1. pose u1 := [ffun i => if (i : 'I_5) == 0 :> nat then ↓[u ord0] else if i == 1 :> nat then s0 else if i == 2 :> nat then t0 else if i == 3 :> nat then ↓[u (inord 1)] else ↓[u (inord 2)]]. have P1 : 2 + sd u1 <= sd u. rewrite /sd 2![in X in X <= _]big_ord_recr [X in _ <= X]big_ord_recr /= !addnA. apply: leq_add; last first. apply: leq_trans (gdist_cunlift _); last by apply: shanoi_connect. rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite !ffunE ![in LHS]inordK //=. by congr(`d[↓[u _],↓[u _]]_smove); apply/val_eqP; rewrite /= !inordK //= -bE bE1. rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite !big_ord_recr big_ord0 /= !ffunE !inordK //= add0n. rewrite -addnA add2n -du0u1. move: bE; rewrite -bE1. case: (l) u => // [] [] // uu _; rewrite big_ord_recl big_ord0 addn0 /=. by congr(`d[uu _, uu _]_smove); apply/val_eqP; rewrite /= !inordK. have cH1 (k : 'I_5) : 0 < k < 4 -> codom (u1 k) \subset [:: p3; a[p1, p2] k]. case: k => [] [|[|[|[|]]]] //= iH _; rewrite !ffunE !(apegS, apeg0). - by have := s0C; rewrite u1LE. - by rewrite codom_subC -KH1. rewrite codom_subC. apply/subsetP=> i /codomP[x ->]; rewrite !ffunE. have /cH: 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK //. by rewrite inordK // => /subsetP /(_ (u (inord 1) (trshift 1 x)) (codom_f _ _)). have {cH1}P2 : (S_[4] n.+1).*2 <= sd u1 + sp (u1 ord0) 4 p1 + sp (u1 ord_max) 4 p1. by apply: IH cH1 => //; rewrite eq_sym. set xP := sd _; rewrite -/xP in P1. have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _ ) (leq_sum_beta _ _)) (leq_sum_beta _ _)). set x1P := sd _ in P1; rewrite -/x1P in P2. rewrite !ffunE /= (_ : inord 2 = ord_max) in P2; last first. by apply: val_inj; rewrite /= inordK // -bE bE1. rewrite {2}(_ : p1 = a[p3, p1] l) in P2; last first. by rewrite -bE -bE1. set x1S := \sum_(_ < _) _ in P2; set x2S := \sum_(_ < _) _ in P2. rewrite !sum_beta_S //= KH1 KH2 !eqxx !addn0 mul1n. rewrite -/x1S -/x2S -!addnA. apply: leq_trans (leq_add P1 (leqnn _)). rewrite -!addnA addnC !addnA -addnA. apply: leq_trans (leq_add P2 (leqnn _)). rewrite -bE -bE1 -addnn {2}dsum_alphaL_S addnA. rewrite [_ + 2]addnC !addnA leq_add2r addnC. by apply: leq_dsum_alpha_2l_l 2 n.+1. have aEl : a = l.+1. apply/eqP; rewrite eqn_leq aLld1 /=. case/orP: oH; first by case: (a) aD1 a_gt0 => [|[|]]. case/orP: o1H; first by case: (a) aD1 a_gt0 => [|[|]]. rewrite /b prednK // => H1 lLa; move: lLa H1. by rewrite leq_eqVlt => /orP[] // /eqP ->; rewrite subSn // subnn eqxx. have bE0 : b = 0 by rewrite /b aEl subnn. 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 < l -> [/\ 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=> iLl. have iLl1 : i < l.+1 by rewrite (leq_trans iLl). apply: sgdistE => //. - by rewrite aMin1 // aEl. - rewrite !aMin1 ?aEl //. by rewrite apegS apeg_eqC. - by rewrite aMin1 ?aEl // eq_sym. - by rewrite aMin1 // aEl. by rewrite aMin1 // aEl. pose u1 := [ffun i => if ((i : 'I_(3 * l).+2) == (3 * l).+1 :>nat) then ↓[u ai] else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))] else if (i %% 3) == 1 then si (i %/ 3) else ti (i %/ 3)]. have u10E : u1 ord0 = ↓[u ord0]. rewrite ffunE /=. by congr (↓[u _]); apply/val_eqP; rewrite /= inordK. have u1mE : u1 ord_max = ↓[u ord_max]. rewrite ffunE eqxx. by congr (↓[u _]); apply/val_eqP/eqP; rewrite /= inordK. have P1 : l.*2 + sd u1 <= sd u. rewrite /sd !big_ord_recr /=. rewrite addnA; apply: leq_add; last first. apply: leq_trans (gdist_cunlift _); last by apply: shanoi_connect. rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite !ffunE !inordK ?eqxx //. rewrite eqn_leq [_ <= _ * _]leqNgt leqnn andbF mod3E /= div3E. congr (`d[↓[u _], ↓[u _]]_smove); apply/val_eqP; rewrite /= ?mulKn //. by rewrite inordK // aiE aEl. rewrite leq_eqVlt; apply/orP; left; apply/eqP. have -> := @sum3E _ (fun i => `d[u1 (inord i), u1 (inord i.+1)]_smove). have -> : l.*2 = \sum_(i < l) 2. by rewrite sum_nat_const /= cardT size_enum_ord muln2. rewrite -big_split /=; apply: eq_bigr => i _. rewrite ffunE !inordK //; last first. by rewrite ltnS ltnW // ltnS leq_mul2l /= ltnW. rewrite eqn_leq [_ <= _ * _]leqNgt ltnS leq_mul2l //=. rewrite (ltnW (ltn_ord _)) andbF mod3E /= div3E. rewrite ffunE !inordK //; last first. by rewrite !ltnS leq_mul2l /= ltnW. rewrite eqn_leq [_.+1 <= _]leqNgt !ltnS leq_mul2l /= [_ <= i]leqNgt. rewrite ltn_ord andbF mod3E /= div3E -[(_ * _).+3](mulnDr 3 1 i) add1n. rewrite ffunE !inordK //; last first. by rewrite!ltnS ltn_mul2l /=. rewrite !mod3E /= !div3E ifN; last first. case: eqP => // eH. have : (3 * i).+2 %% 3 = (3 * l).+1 %% 3 by rewrite eH. by rewrite !mod3E. rewrite ffunE inordK; last first. by rewrite ltnS ltnW // ltnS leq_mul2l /=. rewrite mod3E /= div3E ifN. case: (sitiH i) => //= _ _ ->. by rewrite /= !addnA addn0. case: eqP => // eH. have : (3 * i.+1) %% 3 = (3 * l).+1 %% 3 by rewrite eH. by rewrite !mod3E. have cH1 (k : 'I_(3 * l).+2) : 0 < k < (3 * l).+1 -> codom (u1 k) \subset [:: p2; a[p1, p3] k]. rewrite !ffunE. case: eqP => [->|/eqP kD3l1]; first by rewrite ltnn andbF. case: eqP => [km3E0|/eqP km3D0]. rewrite {1 2 4}(divn_eq k 3) km3E0 addn0. rewrite ltnS mulnC muln_gt0 leq_mul2l /= => /andP[k3_gt0 k3Ll]. rewrite apegMr //. have:= @Hcodom (inord (k %/ 3)); rewrite ffunE inordK //; last first. by apply: leq_trans k3Ll _. by apply; rewrite k3_gt0. case: eqP => [km3E1|/eqP km3D1]. rewrite {1 2 4}(divn_eq k 3) km3E1 addn1 !ltnS /= mulnC ltn_mul2l /= => H1. case: (sitiH (k %/ 3)) => //. by rewrite apegS apegMr // aMin1 ?apegS // aEl ltnS. have km3E2 : k %% 3 = 2. by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 => // [] [|[|]]. rewrite {1 2 4}(divn_eq k 3) km3E2 addn2 /= ltnS => H1. have {}H1 : k %/ 3 < l. by rewrite -[_ < _](ltn_mul2r 3) [l * 3]mulnC (leq_ltn_trans _ H1). rewrite codom_subC. case: (sitiH (k %/ 3)) => // _. rewrite !apegS [_ * 3]mulnC apegMr //. by rewrite aMin1 // (leq_trans H1) // aEl. have {cH1}P2 : (S_[(3 * l).+1] n.+1).*2 <= sd u1 + sp (u1 ord0) (3 * l).+1 p1 + sp (u1 ord_max) (3 * l).+1 (a[p1, p3] (3 * l).+1). by apply: IH cH1. have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leq_sum_beta _ _)). set xP := sd _; rewrite -/xP in P1. set x1P := sd _ in P1. rewrite -/x1P (_ : a[p1, p3] (3 * l).+1 = a[p3, p1] l) in P2; last first. by rewrite apegS apegMr. rewrite !sum_beta_S // KH1 KH2 !eqxx addn0 mul1n. rewrite !ffunE /= eqxx inord_eq0 // (_ : ai = ord_max) in P2; last first. by apply: val_inj; rewrite /= inordK. set x1S := \sum_(_ < _) _ in P2; set x2S := \sum_(_ < _) _ in P2. rewrite -/x1S -/x2S . rewrite -addnn {1}dsum_alphaL_S addnAC !addnA leq_add2r. rewrite -[X in _ <= X]addnA. apply: leq_trans (leq_add P1 (leqnn _)). rewrite -[X in _ <= X]addnA [x1P + _]addnA. apply: leq_trans (leq_add (leqnn _) P2). apply: leq_trans (leq_dsum_alpha_2l_l _ _) _. rewrite addnC; apply: leq_add. by rewrite -addnn -addn1 leq_add. rewrite leq_double. apply: (increasingE (increasing_dsum_alphaL_l _)). by rewrite doubleS ltnS -mul2n ltn_mul2r l_ggt0. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)