proposition: Lemma move_cut (c1 c2 : configuration k n) : move rel c1 c2 -> (ccut c1) != (ccut c2) -> move rel (ccut c1) (ccut c2).
proof: Proof. move => /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2. have [dLt|tLd] := leqP t d. case/eqP: c1Dc2. apply/ffunP => i; rewrite !ffunE. apply: dH2. by rewrite -val_eqE /= neq_ltn (leq_trans _ dLt) // orbT. apply/moveP; exists (Ordinal tLd); split => /=. - by rewrite !ffunE // ordinalK. - move=> /= d2; rewrite !ffunE -val_eqE /= => dDd2. by apply: dH2; rewrite -val_eqE /=. - by apply: on_top_cut. by apply: on_top_cut. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)