proposition: Lemma on_top_cset2 c d (dIsd : d \in sd) : cvalid c -> on_top d c -> on_top (enum_rank_in dIsd d) (cset2 c).
proof: Proof. move=> /= /cvalidP cV /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. apply: dO. apply: (@enum_rank_in_inj _ _ _ _ p0Isp p0Isp) => //. by apply: cV. by apply/cV/enum_valP. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)