Is Query Bound P counting bounded

theorem IsQueryBoundP.counting_bounded [DecidableEq ι] [Fintype ι]    {oa : OracleComp spec α} {n : ℕ}    (h : IsQueryBoundP oa p n)    {z : α × QueryCount ι}    (hz : z ∈ support (countingOracle.simulate oa 0)) :    (∑ i ∈ Finset.univ.filter p, z.2 i) ≤ n := by  induction oa using OracleComp.inductionOn generalizing n z with  | pure x =>      rw [countingOracle.mem_support_simulate_pure_iff] at hz      subst hz      simp  | query_bind t mx ih =>      rw [isQueryBoundP_query_bind_iff] at h      rw [countingOracle.mem_support_simulate_queryBind_iff] at hz      obtain ⟨hne, u, hu⟩ := hz      have hrec :          (∑ i ∈ Finset.univ.filter p, (Function.update z.2 t (z.2 t - 1)) i) ≤            (if p t then n - 1 else n) :=        ih u (h.2 u) hu      have hz_pos : 0 < z.2 t := Nat.pos_of_ne_zero hne      by_cases hpt : p t      · simp only [if_pos hpt] at hrec        rw [sum_filter_update_of_pred_pos hpt hz_pos] at hrec        have hp_pos : 0 < ∑ i ∈ Finset.univ.filter p, z.2 i :=          Nat.lt_of_lt_of_le hz_pos            (Finset.single_le_sum (f := z.2) (fun _ _ => Nat.zero_le _)              (Finset.mem_filter.mpr ⟨Finset.mem_univ t, hpt⟩))        have hn_pos : 0 < n := h.1.resolve_left (fun hnp => hnp hpt)        have hshift : (∑ i ∈ Finset.univ.filter p, z.2 i) - 1 + 1 ≤ (n - 1) + 1 :=          Nat.add_le_add_right hrec 1        rwa [Nat.sub_add_cancel hp_pos, Nat.sub_add_cancel hn_pos] at hshift      · simp only [if_neg hpt] at hrec        rwa [sum_filter_update_of_not_pred hpt] at hrec