proposition: Lemma notin_state_rm p1 p2 z st : p1 != p2 -> ~~ in_state p1 z (rm_state p2 st) -> ~~ in_state p1 z st.
proof: Proof. move=> p1Dp2. elim: st => //= [] [[n p3] v] st IH. case: eqP => /= [<- /IH H1|_ ]. by rewrite negb_or negb_and p1Dp2 H1. by rewrite !negb_or /= => /andP[->]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)