proposition: Lemma subp_or p1 p2 q : p1 <=p q /\ p2 <=p q <-> p1 +p p2 <=p q.
proof: Proof. split=>[[H1] H2 x|H1]; first by case; [move/H1 | move/H2]. by split=>x H2; apply: H1; [left | right]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)