Completeness

theorem completeness' (o : Oracle) (L : o.lipschitz t k) (eve : Bob)    (c0 : 0 < c) (cs : c < s) (q0 : 0 < q) (q1 : q ≤ 1) (v0 : 0 < v) (v1 : v ≤ 1) :    (1 - v) * ((o.final t).prob true - k * c - (1 - (1 - q) ^ (t + 1))) ≤      ((debate (alice c q) eve (vera c s v) t).prob' o).prob true := by  simp only [debate_eq_transposed, transposed, trace, map_bind, ge_iff_le, ←pr_eq_prob]  refine le_trans ?_ (le_pr_bind_of_cut _ (1-v) (alices_success o L c0 q0 q1) ?_ ?_)  · simp only [mul_comm _ (1-v), pr_eq_prob, le_refl]  · intro ⟨p,y⟩ _ h; simp only [pr_map] at h ⊢    have b : (bobs o eve (vera c s v) p y).pr (λ r ↦ ¬extract ((p,y),r) = true) ≤ v := by      simp only [Bool.not_eq_true]; apply evil_bobs_lies o eve cs v0 h.1 h.2    simp only [pr_neg] at b; linarith  · linarith