proposition: Lemma connect_merger m n (c : configuration m) (c1 c2 : configuration n) : connect move c1 c2 -> connect move (cmerge c c1) (cmerge c c2).
proof: Proof. move=> /connectP[x]; rewrite -(path_merger c) => Hp Hl. apply/connectP; eexists; first exact: Hp. by rewrite Hl [RHS]last_map. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)