proposition: Lemma gdist_leq_move p n (c1 c2 : configuration p.+3 n) : `d[c1, c2]_rmove <= (2 ^ n).-1.
proof: Proof. elim: n c1 c2 => [c1 c2 | n IH c1 c2]. rewrite (_ : c1 = c2) ?gdist0 //. by apply/ffunP=> [] [] []. rewrite -[c1]cunliftrK -[c2]cunliftrK. set p1 := c1 ldisk; set p2 := c2 ldisk. have [<-|/eqP p1Dp2] := p1 =P p2. apply: leq_trans. apply: gdist_liftr => [i|]; first by rewrite rirr. apply: connect_move. apply: leq_trans; first by apply: IH. rewrite -ltnS !prednK ?expn_gt0 //. by rewrite leq_exp2l. pose p3 := opeg p1 p2. apply: leq_trans. apply: (@gdist_triangular _ _ _ _ (cliftr p1 `c[p3])). rewrite expnS mul2n -addnn. have tnP : 0 < 2 ^ n by rewrite expn_gt0. rewrite -(prednK tnP) addSn /=. apply: leq_add. apply: leq_trans. apply: gdist_liftr => [i|]; first by rewrite rirr. by apply: connect_move. by apply: IH. apply: leq_trans. apply: (@gdist_triangular _ _ _ _ (cliftr p2 `c[p3])). rewrite gdist_liftr_perfect ?ltnS //; last 3 first. - by apply: rirr. - by rewrite eq_sym opegDl. - by rewrite eq_sym opegDr. apply: leq_trans. apply: gdist_liftr => [i|]; first by rewrite rirr. by apply: connect_move. by apply: IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)