proposition: Lemma subset_disjC p q : {subset p <= predC q} <-> {subset q <= predC p}.
proof: Proof. by split=>H a; apply: contraL (H a). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)