proposition: Lemma disjC s1 s2 : disj s1 s2 = disj s2 s1.
proof: Proof. case: disjP; case: disjP=>//. - by move=>x H1 H2; move/(_ x H2); rewrite H1. by move=>H1 x H2; move/H1; rewrite H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)