proposition: Lemma path_mergel m n (c1 : configuration m) (c2 : configuration n) (cs : seq (configuration _)) : path move (cmerge c1 c2) [seq cmerge i c2 | i <- cs] -> path move c1 cs.
proof: Proof. by elim: cs c1 => //= c3 cs IH c1 /andP[/move_mergel-> /IH]. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)