proposition: Lemma sgdist_pair n (p2 : peg 4) (u v : configuration 4 n.+1) (p1 := u ldisk) (p3 := v ldisk): {st : (configuration 4 n * configuration 4 n) | p1 != p2 -> p1 != p3 -> p2 != p3 -> p1 != p0 -> p2 != p0 -> p3 != p0 -> [/\ codom st.1 \subset [:: p2; p3], codom st.2 \subset [:: p1; p2] & `d[u, v]_smove = D[[:: ↓[u]; st.1; st.2; ↓[v]]].+2]}.
proof: Proof. case: eqP => [_|/eqP p1Dp2]; first by exists (↓[u], ↓[v]). case: eqP => [_|/eqP p1Dp3]; first by exists (↓[u], ↓[v]). case: eqP => [_|/eqP p2Dp3]; first by exists (↓[u], ↓[v]). case: eqP => [_|/eqP p1Dp0]; first by exists (↓[u], ↓[v]). case: eqP => [_|/eqP p2Dp0]; first by exists (↓[u], ↓[v]). case: eqP => [_|/eqP p3Dp0]; first by exists (↓[u], ↓[v]). have pE p : [\/ p = p0, p = p1, p = p2 | p = p3] by apply: pE4. have [cs /= csH] := gpath_connect (shanoi_connect u v). have vIcs : v \in cs. have := mem_last u cs; rewrite (gpath_last csH). rewrite inE; case: eqP => // vEu. by case/eqP : p1Dp3; rewrite /p3 vEu. case: (@split_first _ cs (fun c => c ldisk != p1)) => [|[[sp cs1] cs2]]. apply/negP=> /allP /(_ _ vIcs). rewrite /= -topredE /= negbK. by rewrite eq_sym (negPf p1Dp3). case=> /allP spH spLE csE. pose s := last u cs1. have sMsp : s `-->_s sp. by have := gpath_path csH; rewrite csE cat_path => /and3P[]. have sLp1 : s ldisk = p1. move: (spH s); rewrite /s; case: (cs1) => //= c cs3 /(_ (mem_last _ _)). by rewrite -topredE negbK => /eqP. have spLp0 : sp ldisk = p0. apply/eqP. have /(_ ldisk) := move_diskr sMsp. rewrite eq_sym sLp1 => /(_ spLE) /andP[]. case: (_ =P p0) => // /val_eqP /=. have /eqP/val_eqP/= := p1Dp0. by case: (p1 : nat) => // k; case: (sp _ : nat). have sCd : codom (↓[s]) \subset [:: p2; p3]. apply/subsetP=> i; rewrite !inE => /codomP[j] ->. case: (pE (↓[s] j)) => [||->|->]; rewrite ?eqxx ?orbT //. rewrite ffunE trshift_lift /=. move/eqP; rewrite -spLp0 -[_ == _]negbK; case/negP. apply: move_on_toplDr sMsp _ _; first by rewrite sLp1 spLp0. by rewrite /= /bump [n <= j]leqNgt ltn_ord add0n ltnW. rewrite ffunE trshift_lift /=. move/eqP; rewrite -sLp1 -[_ == _]negbK; case/negP. apply: move_on_toplDl sMsp _ _; first by rewrite sLp1 spLp0. by rewrite /= /bump [n <= j]leqNgt ltn_ord add0n. have vIcs2 : v \in cs2. move: vIcs; rewrite csE !(inE, mem_cat) => /or3P[|/eqP vEs|] //. by move=> /spH; rewrite /= -topredE negbK eq_sym (negPf p1Dp3). by case/eqP : p3Dp0; rewrite /p3 vEs. case: (@split_last _ (sp :: cs2) (fun c => c ldisk != p3)) => [|/= [[t cs3] cs4]/=]. apply/negP=> /allP /(_ _ (mem_head _ _)). by rewrite /= -topredE /= negbK spLp0 eq_sym (negPf p3Dp0). case=> // tLE tH scs2E. have vIcs4 : v \in cs4. have := gpath_last csH; rewrite csE scs2E !last_cat /=. case: (cs4) => /= [tEv|c1 cs5 <-]; last by apply: mem_last. by case/eqP: tLE; rewrite tEv. case: cs4 tH scs2E vIcs4 => // tp cs4 /allP tH scs2E vItpcs4. have tMtp : t `-->_s tp. by have := gpath_path csH; rewrite csE scs2E !cat_path /= => /and5P[]. have tpLp3 : tp ldisk = p3. by move: (tH _ (mem_head _ _)); rewrite /= -topredE negbK => /eqP. have tLp0 : t ldisk = p0. apply/eqP. have /(_ ldisk) := move_diskr tMtp. rewrite tpLp3 => /(_ tLE) /andP[]. case: (_ =P p0) => // /val_eqP /=. have /eqP/val_eqP/= := p3Dp0. by case: (p3 : nat) => // k; case: (t _ : nat). have tCd : codom (↓[t]) \subset [:: p1; p2]. apply/subsetP=> i; rewrite !inE => /codomP[j] ->. case: (pE (↓[t] j)) => [|->|->|]; rewrite ?eqxx ?orbT //. rewrite ffunE trshift_lift /=. move/eqP; rewrite -tLp0 -[_ == _]negbK; case/negP. apply: move_on_toplDl tMtp _ _; first by rewrite tpLp3 tLp0 eq_sym. by rewrite /= /bump [n <= j]leqNgt ltn_ord add0n. rewrite ffunE trshift_lift /=. move/eqP; rewrite -tpLp3 -[_ == _]negbK; case/negP. apply: move_on_toplDr tMtp _ _; first by rewrite tpLp3 tLp0 eq_sym. by rewrite /= /bump [n <= j]leqNgt ltn_ord add0n ltnW. exists (↓[s], ↓[t]); split => //=. rewrite addn0. move: csH; rewrite csE => csH. rewrite (gdist_cat csH) -/s. move: csH => /gpath_catr; rewrite -/s => csH. rewrite gdist_cunlift_eq //; try apply: sirr; last by apply: shanoi_connect. rewrite -!addnS. congr (_ + _). have ->: ↓[s] = ↓[sp]. have sLDspL : s ldisk != sp ldisk by rewrite sLp1 spLp0. apply/ffunP => i; rewrite !ffunE. apply: move_disk1 sMsp sLDspL _. by apply/negP => /eqP/val_eqP /=; rewrite eqn_leq leqNgt ltn_ord. rewrite (gdist_cons csH) addnS; congr (_).+1. move: csH => /gpath_consr csH. have ctEctp : ↓[t] = ↓[tp]. have tLDtpL : t ldisk != tp ldisk by rewrite tLp0 tpLp3 eq_sym. apply/ffunP => i; rewrite !ffunE. apply: move_disk1 tMtp tLDtpL _. by apply/negP => /eqP/val_eqP /=; rewrite eqn_leq leqNgt ltn_ord. case: cs3 scs2E => [[spEt cs2E]|c3 cs3 /= [spE cs2E]]. move: csH; rewrite spEt cs2E => csH. rewrite gdist0 add0n (gdist_cons csH) ctEctp. move: csH => /gpath_consr csH. rewrite gdist_cunlift_eq //; try by apply: sirr. by apply: shanoi_connect. move: csH; rewrite cs2E -cat_rcons => csH. rewrite (gdist_cat csH) last_rcons. rewrite gdist_cunlift_eq //; try apply: sirr; last 2 first. - by apply: shanoi_connect. - by rewrite tLp0. congr (_ + _). move: csH => /gpath_catr; rewrite last_rcons => csH. rewrite (gdist_cons csH); congr (_).+1. move: csH => /gpath_consr csH. rewrite ctEctp gdist_cunlift_eq //; try apply: sirr. by apply: shanoi_connect. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)