proposition: Lemma size_allpairs s t : size [seq f x y | x <- s, y <- t] = size s * size t.
proof: Proof. by elim: s => //= x s IHs; rewrite size_cat size_map IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)