proposition: Lemma on_top_cset c d (dIsd : d \in sd) : on_top d c -> on_top (enum_rank_in dIsd d) (cset c).
proof: Proof. move=> /= /on_topP dO. apply/on_topP => /= d1 H. rewrite leq_eqVlt; case: eqP => //= /eqP dDd1. rewrite -[d1](enum_valK_in dIsd) -sorted_enum_val !enum_rankK_in //; last first. by apply: enum_valP. rewrite ltn_neqAle. case: eqP => [/eqP /val_eqP dEd1 | /eqP dDd1' /=]. by case/eqP: dDd1; rewrite {2}dEd1 enum_valK_in. rewrite !ffunE enum_rankK_in // in H. by apply: dO. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)