Snap dist

lemma snap_dist (alice : Alice) (e0 : 0 < e) : dist o (snap o alice e) ≤ e := by  simp only [dist]; apply csSup_le (Set.range_nonempty _); intro p  simp only [mem_range, forall_exists_index]; intro n h; rw [←h]; clear h  apply csSup_le (Set.range_nonempty _); intro d h  simp only [mem_range] at h; rcases h with ⟨y,h⟩; rw [←h]; clear h  simp only [snap, prob_bind, abs_le]; constructor  · rw [le_sub_iff_add_le, add_comm, ←sub_eq_add_neg, sub_le_iff_le_add]    apply exp_le_of_forall_le; intro q _; simp only [bernoulli_prob_true']    apply max_le (add_nonneg (prob_nonneg _) (le_of_lt e0)); apply min_le_of_right_le    split_ifs with h; linarith [h.1]; linarith  · rw [sub_le_iff_le_add, add_comm, ←sub_le_iff_le_add]    apply le_exp_of_forall_le; intro q _; simp only [bernoulli_prob_true']    apply le_max_of_le_right; apply le_min; linarith [prob_le_one (o _ y) true]    split_ifs with h; linarith; linarith