proposition: Lemma pairwise_relI {T : Type} (r r' : rel T) (s : seq T) : pairwise [rel x y | r x y && r' x y] s = pairwise r s && pairwise r' s.
proof: Proof. by elim: s => //= x s ->; rewrite andbACA all_predI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)