proposition: Lemma move_on_topl n d (c1 c2 : configuration n) : move c1 c2 -> c1 d != c2 d -> on_top d c1.
proof: Proof. case/moveP => d1 [H1 H2 H3 H4 H5]. rewrite (_ : d = d1); first by apply: H3. apply/eqP; case: eqP => /eqP H //. by case/eqP: H5; apply: H2; rewrite eq_sym. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)