proposition: Lemma hdomP h x : x \in hdom h = (x \in dom h) && high x.
proof: Proof. case: h=>[//|[h S]]; rewrite /hdom /= /dom /supp /= =>H. rewrite -!topredE /=. elim: (map key h)=>[|y s IH] //=. case: ifP=>E; rewrite !inE IH; case: eqP=>// -> //=. by rewrite E andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep