proposition: Lemma moveP n (c1 c2 : configuration n) : reflect (exists d1, [/\ r (c1 d1) (c2 d1), forall d2, d1 != d2 -> c1 d2 = c2 d2, on_top d1 c1 & on_top d1 c2]) (move c1 c2).
proof: Proof. apply: (iffP existsP) => [[d /and4P[H1 /forallP H2 H3 H4]]|[d [H1 H2 H3 H4]]]; exists d. by split => // d1 H; apply/eqP/(implyP (H2 _)). rewrite H1 H3 H4 ! andbT /=; apply/forallP => d1; apply/implyP => H. by rewrite H2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)