proposition: Lemma pairwise_all2rel : reflexive r -> symmetric r -> forall xs, pairwise xs = all2rel r xs.
proof: Proof. by move=> r_refl r_sym; elim => //= x xs ->; rewrite all2rel_cons // r_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)