proposition: Lemma disj_remE k (s1 s2 : fmap) : k \notin supp s1 -> disj s1 (rem k s2) = disj s1 s2.
proof: Proof. move=>H; case: disjP; case: disjP=>//; last first. - move=>H1 x; move/H1; rewrite supp_rem inE /= => E. by rewrite (negbTE E) andbF. move=>x H1 H2 H3; move: (H3 x H1) H. rewrite supp_rem inE /= negb_and H2 orbF negbK. by move/eqP=><-; rewrite H1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)