proposition: Lemma spos_rm_state st p p1 : p1 \in spos (rm_state p st) = (p1 != p) && (p1 \in spos st).
proof: Proof. case: p => x y; elim: st => /= [|[[n [x2 y2]] v] st IH]. by rewrite in_nil andbF. case: eqP => /= [[<- <-]|]; rewrite !in_cons IH; first by case: eqP. by do 2 case: eqP => //= ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)