From aef14585099c13908896014f7114e6cc1e7fd061 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Wed, 6 Nov 2024 16:25:59 -0500
Subject: [PATCH] minor cleanup

---
 .../DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean     | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean b/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean
index 7502ac62..13c5fc34 100644
--- a/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean
+++ b/SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean
@@ -9,8 +9,7 @@ import SampCert.DifferentialPrivacy.Queries.UnboundedMax.Properties
 import SampCert.DifferentialPrivacy.Pure.System
 
 noncomputable section
-set_option pp.coercions false
--- set_option pp.all true
+
 open Classical
 
 namespace SLang
@@ -269,7 +268,6 @@ lemma DSN (N : ℕ) (H : Neighbour L1 L2) : ((exactDiffSum N L1) : ℝ) - (exact
         simp only [not_le] at hd
         rw [min_eq_right_iff.mpr ?G1]
         case G1 =>
-          -- #check Nat.add_one_le_iff
           have X : (1 : ℝ) = ((1 : ℕ) : ℝ) := by simp
           rw [X]
           rw [← Nat.cast_add]