proposition: Lemma disjP s1 s2 : disj_spec s1 s2 (disj s1 s2).
proof: Proof. rewrite /disj; case E: (all _ _); first by apply/disj_true/allP. move: E; rewrite all_predC=>/negbFE H. case E: {-1}(supp s1) (H)=>[|k ?]; first by rewrite E. by move/(nth_find k); move: H; rewrite has_find=>/(mem_nth k); apply: disj_false. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)