proposition: Lemma subset_disjE p q : {subset p <= predC q} <-> [predI p & q] =1 pred0.
proof: Proof. split=>H a /=; first by case X: (a \in p)=>//; move/H/negbTE: X. by move=>D; move: (H a); rewrite inE /= D; move/negbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)