proposition: Lemma shanoi_connect_perfect n (c : configuration _ n) p : c `-->* `c[p].
proof: Proof. have sirr := @sirr m.+3. elim: n c p => [c p | n IH c p]; first by apply/eq_connect0/ffunP=> [] [[]]. pose p1 := c ldisk. rewrite -[c]cunliftrK -/p1 -[perfect p]cunliftrK perfect_unliftr ffunE. have [<-|/eqP pDp1] := p =P p1; first by apply/connect_liftr/IH. have [p1Ep0|/eqP p1Dp0] := p1 =P p0. rewrite p1Ep0. case: (so1_cor p) => sDp0 sDp. apply: connect_trans (_ : connect _ ↑[`c[so1 p]]_p _); last first. by apply/connect_liftr/IH. apply: connect_trans (_ : connect _ ↑[`c[so1 p]]_p0 _). by apply/connect_liftr/IH. apply/connect1/move_liftr_perfect; try by rewrite eq_sym. by rewrite /srel /= eq_sym -p1Ep0 pDp1. have [pEp0|/eqP pDp0] := p =P p0. case: (so1_cor p1) => sDp0 sDp1. apply: connect_trans (_ : connect _ ↑[`c[so1 p1]]_p1 _). by apply/connect_liftr/IH. apply: connect_trans (_ : connect _ ↑[`c[so1 p1]]_p _). apply/connect1/move_liftr_perfect; try by rewrite eq_sym. by rewrite /srel /= eq_sym pDp1 pEp0 muln0. by rewrite eq_sym pEp0. by apply/connect_liftr/IH. apply: connect_trans (_ : connect _ ↑[`c[p]]_p1 _). by apply/connect_liftr/IH. apply: connect_trans (_ : connect _ ↑[`c[p]]_p0 _). apply/connect1/move_liftr_perfect; try by rewrite eq_sym. by rewrite /srel /= p1Dp0 muln0. apply: connect_trans (_ : connect _ ↑[`c[p1]]_p0 _). by apply/connect_liftr/IH. apply: connect_trans (_ : connect _ ↑[`c[p1]]_p _). apply/connect1/move_liftr_perfect; try by rewrite // eq_sym. by rewrite /srel /= eq_sym pDp0. by apply/connect_liftr/IH. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi)