proposition: Lemma pairwise_map {T T' : Type} (f : T' -> T) (r : rel T) xs : pairwise r (map f xs) = pairwise (relpre f r) xs.
proof: Proof. by elim: xs => //= x xs ->; rewrite all_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)