proposition: Lemma all2rel_cons x xs : all2rel r (x :: xs) = [&& r x x, all (r x) xs & all2rel r xs].
proof: Proof. rewrite allrel_cons2; congr andb; rewrite andbA -all_predI; congr andb. by elim: xs => //= y xs ->; rewrite rsym andbb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)