proposition: Lemma pairwiseP x0 xs : reflect {in gtn (size xs) &, {homo nth x0 xs : i j / i < j >-> r i j}} (pairwise xs).
proof: Proof. elim: xs => /= [|x xs IHxs]; first exact: (iffP idP). apply: (iffP andP) => [[r_x_xs pxs] i j|Hnth]; rewrite -?topredE /= ?ltnS. by case: i j => [|i] [|j] //= gti gtj ij; [exact/all_nthP | exact/IHxs]. split; last by apply/IHxs => // i j; apply/(Hnth i.+1 j.+1). by apply/(all_nthP x0) => i gti; apply/(Hnth 0 i.+1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)