proposition: Lemma move_sym n (c1 c2 : configuration n) : move c1 c2 = move c2 c1.
proof: Proof. by apply/moveP/moveP=> [] [d [H1 H2 H3 H4]]; exists d; split; rewrite 1?symH 1?eq_sym // => e dDe; apply/sym_equal/H2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)