Alice steps cost

lemma alice_steps_cost (o : Oracle) (bob : Bob) (vera : Vera) (n : ℕ):    (steps (alice c q) bob vera n).cost (fun _ ↦ o) AliceId ≤ n * samples c 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, alice_cost,        Comp.prob_allow_all, add_le_iff_nonpos_right, Comp.cost_allow_all]      refine exp_le_of_forall_le fun _ _ ↦ add_nonpos (by zero_cost) ?_      refine exp_le_of_forall_le fun x m ↦ ?_      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, le_refl]