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