proposition: Lemma Eq_pow_mon1 a b: nonempty b -> a <=s functions b a.
proof: Proof. move => [w wb]. exists (Lf (fun t => Lf (fun _ => t) b a) a (functions b a)). saw; apply: lf_injective. by move => x xa; apply /functionsP; saw;apply:lf_function => t. move => u v ua va /(f_equal (Vf ^~ w)); rewrite !LfV// => s. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)