proposition: Lemma connect_move p n (c1 c2 : configuration p.+3 n) : connect rmove c1 c2.
proof: Proof. elim: n c1 c2 => [c1 c2 | n IH c1 c2]. rewrite (_ : c1 = c2) ?connect0 //. by apply/ffunP=> [] []. rewrite -[c1]cunliftrK -[c2]cunliftrK. set p1 := c1 ldisk; set p2 := c2 ldisk. have [<-|/eqP p1Dp2] := p1 =P p2. by apply: connect_liftr => // i; rewrite rirr. pose p3 := opeg p1 p2. apply: connect_trans (_ : connect _ (cliftr p1 `c[p3]) _). apply: connect_liftr; first by apply: rirr. by apply: IH. apply: connect_trans (_ : connect _ (cliftr p2 `c[p3]) _); last first. apply: connect_liftr; first by apply: rirr. by apply: IH. apply: connect1. apply: move_liftr_perfect => //. rewrite eq_sym; apply: opegDl. rewrite eq_sym; apply: opegDr. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)