proposition: Lemma map_allpairs S T R R' (g : R' -> R) f s t : map g [seq f x y | x : S <- s, y : T x <- t x] = [seq g (f x y) | x <- s, y <- t x].
proof: Proof. by rewrite map_flatten allpairs_mapl allpairs_mapr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)