# HG changeset patch
# User paulson
# Date 1519340318 0
# Node ID 3c02b0522e230e951869308638d6fd3a041e4ead
# Parent  34e0e0d5ea7cfa2747d0deaba3034af44cd875d8# Parent  2c38ffd6ec71d7865c18db4473c8bd8c5b745f07
merged

diff -r 34e0e0d5ea7c -r 3c02b0522e23 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Thu Feb 22 20:05:30 2018 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Thu Feb 22 22:58:38 2018 +0000
@@ -383,6 +383,8 @@
     by (simp split: enat.splits)
   show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat
     by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto
+  show "a < b \<Longrightarrow> a + 1 < b + 1"
+    by (metis add_right_mono eSuc_minus_1 eSuc_plus_1 less_le)
 qed (simp add: zero_enat_def one_enat_def)
 
 (* BH: These equations are already proven generally for any type in
diff -r 34e0e0d5ea7c -r 3c02b0522e23 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Feb 22 20:05:30 2018 +0100
+++ b/src/HOL/Rings.thy	Thu Feb 22 22:58:38 2018 +0000
@@ -2245,7 +2245,8 @@
 
 end
 
-class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
+class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one +
+  assumes add_mono1: "a < b \<Longrightarrow> a + 1 < b + 1"
 begin
 
 subclass zero_neq_one
@@ -2278,7 +2279,15 @@
   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
 begin
 
-subclass linordered_nonzero_semiring ..
+subclass linordered_nonzero_semiring 
+proof
+  show "a + 1 < b + 1" if "a < b" for a b
+  proof (rule ccontr, simp add: not_less)
+    assume "b \<le> a"
+    with that show False
+      by (simp add: )
+  qed
+qed
 
 text \<open>Addition is the inverse of subtraction.\<close>