proposition: Lemma nonempty_image f x: function f -> nonempty x -> sub x (source f) -> nonempty (Vfs f x).
proof: Proof. move=> ff [z zx] xf; exists (Vf f z); apply/dirim_P; ex_tac; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)