proposition: Lemma on_top_clmerge x c : on_top x c -> on_top (tlshift m x) (clmerge c).
proof: Proof. move=> /on_topP oH; apply/on_topP => d. rewrite !ffunE tsplit_tlshift /=. case: tsplitP => y; rewrite !ffunE => ->. case: (_ == _) => [/eqP|]; first by rewrite (negPf p1Dp3). case: (_ == _) => /eqP; first by rewrite eq_sym (negPf p3Dp0). by rewrite (negPf p2Dp3). case: eqP => [cxE0|cxD0]. case: eqP => [cyE0 _| _]. by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE0. by case: (_ == _) => /eqP; rewrite (negPf p1Dp0, negPf p1Dp2). case: eqP => [cxE1|cxD1]. case: (_ == _) => [/eqP|]; first by rewrite eq_sym (negPf p1Dp0). case: eqP => [cyE1 _|_ /eqP]. by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE1. by rewrite eq_sym (negPf p2Dp0). have cxE2 : c x = 2 :> nat by case: (c x) cxD0 cxD1 => [] [|[|[]]]. case: eqP => [_ /eqP|cyD0]. by rewrite eq_sym (negPf p1Dp2). case: eqP => [_ /eqP|cyD1 _]. by rewrite (negPf p2Dp0). have cyE2 : c y = 2 :> nat by case: (c y) cyD0 cyD1 => [] [|[|[]]]. by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)