proposition: Lemma in_allpairs (S T R : eqType) (f : S -> T -> R) (s : seq S) (t : seq T) x y : injective (uncurry f) -> f x y \in [seq f x0 y0 | x0 <- s, y0 <- t] = (x \in s) && (y \in t).
proof: Proof. move=> f_inj; apply/allpairsP/andP => [|[]]; last by exists (x, y). by case=> -[/= x' y'] [x's y't] /(f_inj (x, y) (x',y')) [-> ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)