proposition: Lemma dom_null h x : x \in dom h -> x != null.
proof: Proof. by case: h=>[|h H1] //; case: eqP=>// ->; rewrite (negbTE H1). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep