proposition: Lemma move_on_toplDr n (d d1 : disk n) (c1 c2 : configuration n) : move c1 c2 -> c1 d != c2 d -> d1 <= d -> c1 d1 != c2 d.
proof: Proof. move=> c1Mc2 c1Dc2; rewrite leq_eqVlt => /orP[/val_eqP->//|dLd1]. move: (dLd1); rewrite eq_sym ltnNge (move_disk1 c1Mc2 c1Dc2) //; last first. by rewrite neq_ltn dLd1 orbT. apply: contra => /eqP. by have /on_topP := move_on_topr c1Mc2 c1Dc2; apply. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)