proposition: Lemma subp_and p1 p2 q : 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: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)