proposition: Lemma move_on_toprDr n (d d1 : disk n) (c1 c2 : configuration n) : move c1 c2 -> c1 d != c2 d -> d1 < d -> c2 d1 != c2 d.
proof: Proof. move=> c1Mc2 c1Dc2; rewrite eq_sym ltnNge; apply: contra => /eqP. by have /on_topP := move_on_topr c1Mc2 c1Dc2; apply. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)