proposition: Lemma pairwise_cat xs ys : pairwise (xs ++ ys) = [&& allrel r xs ys, pairwise xs & pairwise ys].
proof: Proof. by elim: xs => //= x xs ->; rewrite all_cat -!andbA; bool_congr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)