Bob steps cost

lemma bob_steps_cost (o : Oracle) (alice : Alice) (vera : Vera) (n : ℕ):    (steps alice (bob s b q) vera n).cost (fun _ ↦ o) BobId ≤ n * samples ((b-s)/2) q := by  induction' n with n h  · simp only [Nat.zero_eq, steps, Comp.cost_pure, CharP.cast_eq_zero, zero_mul, le_refl]  · simp only [steps, Comp.cost_bind, Nat.cast_succ, add_mul, one_mul]    refine add_le_add h (exp_le_of_forall_le (fun y m ↦ ?_))    induction y    · simp only [Comp.cost_pure, Nat.cast_nonneg]    · simp only [step, Comp.sample'_bind, pure_bind, Comp.cost_bind, Comp.cost_allow_all,        Comp.prob_allow_all]      have b0 : ∀ y o, (alice n y).cost o BobId = 0 := by intro _ _; zero_cost      rw [b0, zero_add]      refine exp_le_of_forall_le fun _ _ ↦ ?_      simp only [bob_cost, add_le_iff_nonpos_right]      refine (exp_eq_zero fun x _ ↦ ?_).le      induction x      · simp only [ite_false, Comp.cost_bind, Comp.cost_allow_all, Comp.prob_allow_all,          Comp.cost_pure, exp_const, add_zero]        zero_cost      · simp only [ite_true, Comp.cost_sample, Comp.cost_pure, exp_const]