proposition: Lemma disj_rem k (s1 s2 : fmap) : disj s1 s2 -> disj s1 (rem k s2).
proof: Proof. case: disjP=>// H _; case: disjP=>// x; move/H. by rewrite supp_rem inE /= andbC; move/negbTE=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)