src/HOL/Groups.thy

--- a/src/HOL/Groups.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Groups.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -639,11 +639,6 @@
 
 end
 
-lemma mono_add:
-  fixes a :: "'a::ordered_ab_semigroup_add" 
-  shows "mono ((+) a)"
-  by (simp add: add_left_mono monoI)
-
 text \<open>Strict monotonicity in both arguments\<close>
 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"