proposition: Lemma move_tuc (c1 c2 : configuration k n) : move rel c1 c2 -> (ctuc c1) != (ctuc c2) -> move rel (ctuc c1) (ctuc c2).
proof: Proof. move => /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2. have [dLt|tLd] := leqP t d; last first. case/eqP: c1Dc2. apply/ffunP => i; rewrite !ffunE. apply: dH2. by rewrite -val_eqE /= neq_ltn (leq_trans tLd _) // leq_addl. apply/moveP; exists (otuc dLt); split => /=. - by rewrite !ffunE // otucK. - move=> /= d2; rewrite !ffunE -val_eqE /= => dDd2. by apply: dH2; rewrite -val_eqE /= -(subnK dLt) eqn_add2r. - by apply: on_top_tuc. by apply: on_top_tuc. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)