proposition: Lemma sub_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) : {in P &, subrel r r'} -> forall xs, all P xs -> pairwise r xs -> pairwise r' xs.
proof: Proof. move=> rr'; elim=> //= x xs IHxs /andP [Px Pxs] /andP [+ {}/IHxs->] //. rewrite andbT; elim: xs Pxs => //= x' xs IHxs /andP [? ?] /andP [+ /IHxs->] //. by rewrite andbT; apply: rr'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)