proposition: Lemma disj_ins k v (s1 s2 : fmap) : disj s1 (ins k v s2) = (k \notin supp s1) && (disj s1 s2).
proof: Proof. case: disjP=>[H|x H1]. - case E: (k \in supp s1)=>/=. - by move: (H _ E); rewrite supp_ins inE /= eq_refl. case: disjP=>// x H1 H2. by move: (H _ H1); rewrite supp_ins inE /= H2 orbT. rewrite supp_ins inE /=; case/orP=>[|H2]. - by move/eqP=><-; rewrite H1. rewrite andbC; case: disjP=>[H|y H3 H4] //=. by move: (H _ H1); rewrite H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)