proposition: Lemma valid_state_fold (A : Type) (st : state) (s : seq A) h1 f1 z : valid_state st -> valid_state (foldr (fun (x1 : A) st0 => if h1 x1 then st0 else update_state (f1 x1) z st0) st s).
proof: Proof. elim: s st => [|x s IH] st Hu //=. case: (h1 _) => //=; first by apply: IH. by apply/valid_state_update/IH. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)