proposition: Lemma perm_spos_update p i st : perm_eq (spos (update_state p i st)) (spos st).
proof: Proof. elim: st => //= [] [[n1 p1] i1] st IH. case: eqP => /= [<-|_]; first by apply: perm_spos_add. apply: perm_trans (perm_spos_add _ _ _ _) _. by rewrite perm_cons. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)