proposition: Lemma on_top_tuc c (d : disk n) (dLr : t <= d) : on_top d c -> on_top (otuc dLr) (ctuc c).
proof: Proof. move=> /= /on_topP dO. apply/on_topP => /= d1 H. rewrite leq_eqVlt; case: eqP => //= /eqP dDd1. rewrite ltn_neqAle dDd1 /= leq_subLR addnC. apply: (dO (tuc_ord d1)) => //. by move: H; rewrite !ffunE otucK. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)