proposition: Lemma Vg_out_of_range f x: ~ inc x (domain f) -> Vg f x = emptyset.
proof: Proof. move => idx; rewrite /Vg /select; set T := Zo _ _. case:(emptyset_dichot T); first by move ->; rewrite setU_0. by move => [y /Zo_P [_ /domain_i idf]]; case: idx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)