proposition: Lemma perm_spos_add n p i st : perm_eq (spos (add_state n p i st)) (p :: spos st).
proof: Proof. elim: st => //= [] [[n1 p1] i1] st IH. case: leqP => //= _. by rewrite perm_sym -perm_rcons /= perm_cons perm_rcons perm_sym. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)