proposition: Lemma Eq_mul_mon1 a b: nonempty b -> a <=s a \times b.
proof: Proof. move =>[x xb]; exists (Lf (fun z => J z x) a (a\times b)); saw. apply: lf_injective; first by move => z za; apply: setXp_i. by move => u v _ _ /pr1_def. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)