proposition: Lemma allpairs_rconsr f s y0 t : perm_eql [seq f x y | x <- s, y <- rcons (t x) (y0 x)] ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]).
proof: Proof. apply/permPl; rewrite -(eq_allpairsr _ _ (fun=> cats1 _ _)). by rewrite perm_allpairs_catr allpairs1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)