proposition: Lemma fun_set_ne x y: (x = emptyset \/ nonempty y) -> nonempty (functions x y).
proof: Proof. case=> p. rewrite p;move: (empty_function_tg_function y) => h. by exists (empty_function_tg y); apply/functionsP. move: p => [p py]; exists (constant_function x y p); apply/functionsP. by apply constant_prop. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)