Vera debate cost

theorem vera_debate_cost (o : Oracle) (alice : Alice) (bob : Bob) (t : ℕ):    (debate alice bob (vera c s v) t).cost' o VeraId ≤ samples ((s-c)/2) v := by  have z : (stepsV alice bob (t+1)).cost (fun _ ↦ o) VeraId = 0 := by zero_cost  simp only [Comp.cost', debate, ← post_stepsV, bind_assoc, Comp.cost_bind, Comp.cost_allow_all, z,    Comp.prob_allow_all, zero_add, ge_iff_le]  refine exp_le_of_forall_le fun x _ ↦ ?_  refine le_trans (add_le_of_nonpos_right ?_) ?_  · refine exp_le_of_forall_le fun x _ ↦ ?_    induction x; repeat simp only [Comp.cost_pure, le_refl]  · simp only [postV]    induction x    · simp only [Comp.cost_bind, Comp.cost_allow_all, vera_cost, Comp.prob_allow_all,        Comp.cost_pure, exp_const, add_zero, le_refl]    · simp only [Comp.cost_pure, Nat.cast_nonneg]