proposition: Lemma valid_state_update p z (st : state) : valid_state st -> valid_state (update_state p z st).
proof: Proof. move=> [Hu Hv Hw]; split. - by rewrite (perm_uniq (perm_spos_update _ _ _)) Hu /=. - move=> p1 Hp1; apply: Hv. by rewrite (perm_mem (perm_spos_update _ _ _)) in Hp1. by move=> p1 z1; rewrite in_state_update // => /andP[_ /Hw]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)