proposition: Lemma allpairsP f s t (z : R) : reflect (exists p, [/\ p.1 \in s, p.2 \in t & z = f p.1 p.2]) (z \in [seq f x y | x <- s, y <- t]).
proof: Proof. by apply: (iffP allpairsPdep) => [[x[y]]|[[x y]]]; [exists (x, y)|exists x, y]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)