diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean
index 7aa6542..ad03af2 100644
--- a/lean/Spa/Analysis/Constant.lean
+++ b/lean/Spa/Analysis/Constant.lean
@@ -31,20 +31,12 @@ theorem plus_mono₂ : Monotone₂ plus :=
     (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
     (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
 
-theorem plus_mono_left (s₂ : ConstLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂
-
-theorem plus_mono_right (s₁ : ConstLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁
-
 theorem minus_mono₂ : Monotone₂ minus :=
   AboveBelow.monotone₂_of_strict minus
     (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
     (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
     (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
 
-theorem minus_mono_left (s₂ : ConstLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂
-
-theorem minus_mono_right (s₁ : ConstLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁
-
 def interpConst : ConstLattice → Value → Prop
   | .bot, _ => False
   | .top, _ => True
diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean
index 842ba23..51c2fed 100644
--- a/lean/Spa/Analysis/Sign.lean
+++ b/lean/Spa/Analysis/Sign.lean
@@ -62,10 +62,6 @@ theorem plus_mono₂ : Monotone₂ plus :=
       rcases x with _ | _ | s <;>
         first | exact absurd rfl hx | rfl | (cases s <;> rfl))
 
-theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂
-
-theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁
-
 theorem minus_mono₂ : Monotone₂ minus :=
   AboveBelow.monotone₂_of_strict minus
     (fun y => by cases y <;> rfl)
@@ -75,10 +71,6 @@ theorem minus_mono₂ : Monotone₂ minus :=
       rcases x with _ | _ | s <;>
         first | exact absurd rfl hx | rfl | (cases s <;> rfl))
 
-theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂
-
-theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁
-
 def interpSign : SignLattice → Value → Prop
   | .bot, _ => False
   | .top, _ => True