proposition: Lemma path_move_rev (n : nat) (c : configuration n) cs : path move (last c cs) (rev (belast c cs)) = path move c cs.
proof: Proof. by rewrite rev_path; apply: eq_path => c1 c2; exact: move_sym. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)