fact: Definition Ex1_2_hD r f := forall x y x', gle r x y -> inc x' (source f) -> Vf f x = Vf f x' -> exists y', [/\ inc y' (source f), gle r x' y' & Vf f y = Vf f y'].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)