proposition: Lemma gdist_leq (n : nat) (p1 p2 : peg 4) : `d[`c[p1, n], `c[p2, n]]_rmove <= ϕ(n).
proof: Proof. have [/eqP->|p1Dp2] := boolP (p1 == p2); first by rewrite gdist0. elim/ltn_ind: n p1 p2 p1Dp2 => [] [|[|n]] IH p1 p2 p1Dp2. - rewrite (_ : `c[p1] = `c[p2]) ?gdist0 //. by apply/ffunP => [] []. - rewrite -[phi 1]/(size [:: `c[p2, 1]]). apply: gdist_path_le => //=. rewrite andbT; apply/moveP; exists ldisk; split => //=. - by rewrite !ffunE. - by move=> [[|]]. - by apply/on_topP => [] []. by apply/on_topP => [] []. pose p3 := `p[p1, p2]. set k := gmin n.+2. set k1 := k.-1.+1. have kP : 0 < k by apply: gmin_gt0. have k1Lm2 : k1 < n.+2 by rewrite [k1]prednK //; apply: gmin_lt. have k1Lm2S : k1 <= n.+2 by apply: ltnW. rewrite -[in X in X <= _](subnK k1Lm2S); set k2 := _ - _. rewrite -perfect_liftrn; set c1 := cliftrn _ _ _. rewrite -perfect_liftrn; set c4 := cliftrn _ _ _. pose c2 : _ _ (k2 + k1) := cliftrn k2 p1 `c[p3]. pose c3 : _ _ (k2 + k1) := cliftrn k2 p2 `c[p3]. apply: leq_trans (_ : _ <= gdist rmove c1 c2 + _) _. by apply: gdist_triangular. rewrite phi_gmin /g -/k -/k1 -addnn -addnA. apply: leq_add. apply: leq_trans. apply: gdist_merger; first by apply: rirr. by apply: connect_move. rewrite -(prednK kP). apply: IH => //. by rewrite eq_sym opegDl. apply: leq_trans (_ : _ <= gdist rmove c2 c3 + _) _. by apply: gdist_triangular. rewrite addnC. apply: leq_add. apply: leq_trans. apply: gdist_merger; first apply: rirr. by apply: connect_move. rewrite -(prednK kP). apply: IH => //. by rewrite opegDr. rewrite /c2 /c3; move: p1Dp2. have [p2' -> p2'E] := unlift_some (opegDr p1 p2). rewrite -/p3. have [p1' -> p1'E] := unlift_some (opegDl p1 p2). move => p1Dp2. have p1'Dp2' : p1' != p2' by apply: contra p1Dp2 => /eqP->. rewrite -[X in _ <= X]muln1 {11}(_ : 1 = (p1' != p2')); last first. by rewrite (negPf p1'Dp2'). rewrite -gdist_rhanoi3p -/p3 -!crliftn_perfect -!plift_perfect. rewrite -(prednK kP). apply: gdist_liftln => [|i j|]; first by apply: rirr. by (apply/idP/idP; apply: contra => /eqP) => [/lift_inj->|->]. by apply: move_connect. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist ghanoi ghanoi4 triangular phi rhanoi3 psi)