proposition: Lemma path_clmerge c cs : path (move (@lrel 3)) c cs -> path smove (clmerge c) [seq clmerge c | c <- cs].
proof: Proof. elim: cs c => //= c1 cs IH c2 /andP[mH pH]. by rewrite move_clmerge // IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)