proposition: Lemma on_topP n (d : disk n) (c : configuration n) : reflect (forall d1, c d = c d1 -> d <= d1) (on_top d c).
proof: Proof. apply: (iffP forallP) => [H d1 cdEcd1|H d1]. by have /implyP->// := H d1; apply/eqP. by apply/implyP=> /eqP /H. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)