fact: Fixpoint update_state p i st := if st is ((n1, p1, bs1) as t) :: st1 then if p == p1 then let bs2 := rm_val i bs1 in add_state (rank_val bs2) p bs2 st1 else add_state n1 p1 bs1 (update_state p i st1) else [::].
imports: mathcomp(all_ssreflect) mathcomp(zify)