proposition: Lemma move_clmerge c1 c2 : lmove c1 c2 -> clmerge c1 `-->_s clmerge c2.
proof: Proof. move=> /moveP [d1 [H1d1 H2d1 H3d1 H4d1]]. apply/moveP; exists (tlshift m d1); split => //. - move: H1d1; rewrite !ffunE tsplit_tlshift !ffunE. rewrite /lrel /= /srel /ghanoi.srel /=. case: (c1 d1) => [] [|[|[|]]] //=. - case: (c2 d1) => [] [|[|[|]]] //=. by rewrite p1Dp0 muln0. - case: (c2 d1) => [] [|[|[|]]] //= _ _ _. by rewrite eq_sym p1Dp0. by rewrite eq_sym p2Dp0. case: (c2 d1) => [] [|[|[|]]] //= _ _ _. by rewrite p2Dp0 muln0. - move=> d2; rewrite !ffunE; case: tsplitP => j; rewrite !ffunE //. move=> d2E /eqP/val_eqP. rewrite /= d2E eqn_add2r => H. by rewrite (@H2d1 j). - by apply: on_top_clmerge. by apply: on_top_clmerge. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)