proposition: Lemma subp_and (p1 p2 q : Pred T) : q <=p p1 /\ q <=p p2 <-> q <=p p1 *p p2.
proof: Proof. split=>[[H1] H2 x|] H; last by split=>x; case/H. by split; [apply: H1 | apply: H2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool seq) Setoid