proposition: Lemma path_mergel_inv m n (c1 : configuration m) (c2 : configuration n) (cs : seq (configuration _)) : all (fun i => cdisjoint i c2) (c1 :: cs) -> path move c1 cs -> path move (cmerge c1 c2) [seq cmerge i c2 | i <- cs].
proof: Proof. elim: cs c1 => //= c3 cs IH c1 /and3P[c1Dc2 c3Dc2 Dcs] /andP[/move_mergel_inv ->// /IH->//]. by rewrite c3Dc2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)