proposition: Lemma allpairs_rcons f x s t : [seq f x y | x <- rcons s x, y <- t x] = [seq f x y | x <- s, y <- t x] ++ [seq f x y | y <- t x].
proof: Proof. by rewrite -cats1 allpairs_cat allpairs1l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)