# HG changeset patch
# User haftmann
# Date 1581285522 0
# Node ID f2da99316b869bf932bfa026296c4b0bbbb6a104
# Parent  e83fe2c31088ecf978ecd45f1ee5de9062aa36ee
more rules for natural deduction from inequalities

diff -r e83fe2c31088 -r f2da99316b86 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Feb 09 10:46:32 2020 +0000
+++ b/src/HOL/Groups.thy	Sun Feb 09 21:58:42 2020 +0000
@@ -1413,6 +1413,25 @@
 lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y \<longleftrightarrow> x = 0 \<and> y = 0"
   using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] .
 
+lemma less_eqE:
+  assumes \<open>a \<le> b\<close>
+  obtains c where \<open>b = a + c\<close>
+  using assms by (auto simp add: le_iff_add)
+
+lemma lessE:
+  assumes \<open>a < b\<close>
+  obtains c where \<open>b = a + c\<close> and \<open>c \<noteq> 0\<close>
+proof -
+  from assms have \<open>a \<le> b\<close> \<open>a \<noteq> b\<close>
+    by simp_all
+  from \<open>a \<le> b\<close> obtain c where \<open>b = a + c\<close>
+    by (rule less_eqE)
+  moreover have \<open>c \<noteq> 0\<close> using \<open>a \<noteq> b\<close> \<open>b = a + c\<close>
+    by auto
+  ultimately show ?thesis
+    by (rule that)
+qed
+
 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
   \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
 
diff -r e83fe2c31088 -r f2da99316b86 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Feb 09 10:46:32 2020 +0000
+++ b/src/HOL/Nat.thy	Sun Feb 09 21:58:42 2020 +0000
@@ -793,7 +793,6 @@
    apply simp_all
   done
 
-text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
 lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
 proof (induct n)
   case 0
@@ -809,6 +808,11 @@
   for k l :: nat
   by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
 
+lemma less_natE:
+  assumes \<open>m < n\<close>
+  obtains q where \<open>n = Suc (m + q)\<close>
+  using assms by (auto dest: less_imp_Suc_add intro: that)
+
 text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
 lemma mult_less_mono2:
   fixes i j :: nat