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