src/HOL/Nat.thy
 changeset 62481 b5d8e57826df parent 62378 85ed00c1fe7c child 62502 8857237c3a90
```     1.1 --- a/src/HOL/Nat.thy	Tue Mar 01 10:32:55 2016 +0100
1.2 +++ b/src/HOL/Nat.thy	Tue Mar 01 10:36:19 2016 +0100
1.3 @@ -8,14 +8,13 @@
1.4  section \<open>Natural numbers\<close>
1.5
1.6  theory Nat
1.7 -imports Inductive Typedef Fun Fields
1.8 +imports Inductive Typedef Fun Rings
1.9  begin
1.10
1.11  ML_file "~~/src/Tools/rat.ML"
1.12
1.13  named_theorems arith "arith facts -- only ground formulas"
1.14  ML_file "Tools/arith_data.ML"
1.15 -ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
1.16
1.17
1.18  subsection \<open>Type \<open>ind\<close>\<close>
1.19 @@ -724,11 +723,16 @@
1.20    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
1.21
1.22  text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
1.23 -lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
1.24 -apply(auto simp: gr0_conv_Suc)
1.25 -apply (induct_tac m)
1.27 -done
1.28 +lemma mult_less_mono2:
1.29 +  fixes i j :: nat
1.30 +  assumes "i < j" and "0 < k"
1.31 +  shows "k * i < k * j"
1.32 +using \<open>0 < k\<close> proof (induct k)
1.33 +  case 0 then show ?case by simp
1.34 +next
1.35 +  case (Suc k) with \<open>i < j\<close> show ?case
1.37 +qed
1.38
1.39  text \<open>Addition is the inverse of subtraction:
1.40    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
1.41 @@ -1103,8 +1107,18 @@
1.42  lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
1.43  by (induct j k rule: diff_induct) simp_all
1.44
1.46 +  fixes i j k :: nat
1.47 +  shows "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
1.48 +  by (fact diff_add_assoc [symmetric])
1.49 +
1.50  lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
1.52 +  by (simp add: ac_simps)
1.53 +
1.55 +  fixes i j k :: nat
1.56 +  shows "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
1.57 +  by (fact diff_add_assoc2 [symmetric])
1.58
1.59  lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
1.60  by auto
1.61 @@ -1457,6 +1471,14 @@
1.62
1.63  declare of_nat_code [code]
1.64
1.65 +context ring_1
1.66 +begin
1.67 +
1.68 +lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
1.70 +
1.71 +end
1.72 +
1.73  text\<open>Class for unital semirings with characteristic zero.
1.74   Includes non-ordered rings like the complex numbers.\<close>
1.75
1.76 @@ -1485,6 +1507,8 @@
1.77
1.78  end
1.79
1.80 +class ring_char_0 = ring_1 + semiring_char_0
1.81 +
1.82  context linordered_semidom
1.83  begin
1.84
1.85 @@ -1521,14 +1545,6 @@
1.86
1.87  end
1.88
1.89 -context ring_1
1.90 -begin
1.91 -
1.92 -lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
1.94 -
1.95 -end
1.96 -
1.97  context linordered_idom
1.98  begin
1.99
1.100 @@ -1621,21 +1637,6 @@
1.101    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
1.102    \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
1.103
1.104 -ML_file "Tools/lin_arith.ML"
1.105 -setup \<open>Lin_Arith.global_setup\<close>
1.106 -declaration \<open>K Lin_Arith.setup\<close>
1.107 -
1.108 -simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
1.109 -  \<open>K Lin_Arith.simproc\<close>
1.110 -(* Because of this simproc, the arithmetic solver is really only
1.111 -useful to detect inconsistencies among the premises for subgoals which are
1.112 -*not* themselves (in)equalities, because the latter activate
1.113 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
1.114 -solver all the time rather than add the additional check. *)
1.115 -
1.116 -
1.117 -lemmas [arith_split] = nat_diff_split split_min split_max
1.118 -
1.119  context order
1.120  begin
1.121
1.122 @@ -1695,62 +1696,95 @@
1.123
1.124  text\<open>Subtraction laws, mostly by Clemens Ballarin\<close>
1.125
1.126 -lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
1.127 -by arith
1.128 -
1.129 -lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
1.130 -by arith
1.131 +lemma diff_less_mono:
1.132 +  fixes a b c :: nat
1.133 +  assumes "a < b" and "c \<le> a"
1.134 +  shows "a - c < b - c"
1.135 +proof -
1.136 +  from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0"
1.138 +  then show ?thesis by simp
1.139 +qed
1.140 +
1.141 +lemma less_diff_conv:
1.142 +  fixes i j k :: nat
1.143 +  shows "i < j - k \<longleftrightarrow> i + k < j" (is "?P \<longleftrightarrow> ?Q")
1.144 +  by (cases "k \<le> j")
1.146
1.147  lemma less_diff_conv2:
1.148    fixes j k i :: nat
1.149    assumes "k \<le> j"
1.150 -  shows "j - k < i \<longleftrightarrow> j < i + k"
1.151 -  using assms by arith
1.152 -
1.153 -lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
1.154 -by arith
1.155 -
1.156 -lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
1.157 -by arith
1.158 -
1.159 -(*Replaces the previous diff_less and le_diff_less, which had the stronger
1.160 -  second premise n\<le>m*)
1.161 -lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
1.162 -by arith
1.163 +  shows "j - k < i \<longleftrightarrow> j < i + k" (is "?P \<longleftrightarrow> ?Q")
1.164 +  using assms by (auto dest: le_Suc_ex)
1.165 +
1.166 +lemma le_diff_conv:
1.167 +  fixes j k i :: nat
1.168 +  shows "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
1.169 +  by (cases "k \<le> j")
1.171 +
1.172 +lemma diff_diff_cancel [simp]:
1.173 +  fixes i n :: nat
1.174 +  shows "i \<le> n \<Longrightarrow> n - (n - i) = i"
1.175 +  by (auto dest: le_Suc_ex)
1.176 +
1.177 +lemma diff_less [simp]:
1.178 +  fixes i n :: nat
1.179 +  shows "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
1.180 +  by (auto dest: less_imp_Suc_add)
1.181
1.182  text \<open>Simplification of relational expressions involving subtraction\<close>
1.183
1.184 -lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
1.185 -by (simp split add: nat_diff_split)
1.186 +lemma diff_diff_eq:
1.187 +  fixes m n k :: nat
1.188 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
1.189 +  by (auto dest!: le_Suc_ex)
1.190
1.191  hide_fact (open) diff_diff_eq
1.192
1.193 -lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
1.194 -by (auto split add: nat_diff_split)
1.195 -
1.196 -lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
1.197 -by (auto split add: nat_diff_split)
1.198 -
1.199 -lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
1.200 -by (auto split add: nat_diff_split)
1.201 +lemma eq_diff_iff:
1.202 +  fixes m n k :: nat
1.203 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
1.204 +  by (auto dest: le_Suc_ex)
1.205 +
1.206 +lemma less_diff_iff:
1.207 +  fixes m n k :: nat
1.208 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
1.209 +  by (auto dest!: le_Suc_ex)
1.210 +
1.211 +lemma le_diff_iff:
1.212 +  fixes m n k :: nat
1.213 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
1.214 +  by (auto dest!: le_Suc_ex)
1.215
1.216  text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
1.217
1.218 -(* Monotonicity of subtraction in first argument *)
1.219 -lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
1.220 -by (simp split add: nat_diff_split)
1.221 -
1.222 -lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
1.223 -by (simp split add: nat_diff_split)
1.224 -
1.225 -lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
1.226 -by (simp split add: nat_diff_split)
1.227 -
1.228 -lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
1.229 -by (simp split add: nat_diff_split)
1.230 -
1.231 -lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
1.232 -by auto
1.233 +lemma diff_le_mono:
1.234 +  fixes m n l :: nat
1.235 +  shows "m \<le> n \<Longrightarrow> m - l \<le> n - l"
1.237 +
1.238 +lemma diff_le_mono2:
1.239 +  fixes m n l :: nat
1.240 +  shows "m \<le> n \<Longrightarrow> l - n \<le> l - m"
1.241 +  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
1.242 +
1.243 +lemma diff_less_mono2:
1.244 +  fixes m n l :: nat
1.245 +  shows "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
1.247 +
1.248 +lemma diffs0_imp_equal:
1.249 +  fixes m n :: nat
1.250 +  shows "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
1.251 +  by (simp split add: nat_diff_split)
1.252 +
1.253 +lemma min_diff:
1.254 +  fixes m n i :: nat
1.255 +  shows "min (m - i) (n - i) = min m n - i" (is "?lhs = ?rhs")
1.256 +  by (cases m n rule: le_cases)
1.257 +    (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
1.258
1.259  lemma inj_on_diff_nat:
1.260    assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
1.261 @@ -1759,78 +1793,130 @@
1.262    fix x y
1.263    assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
1.264    with k_le_n have "x - k + k = y - k + k" by auto
1.265 -  with a k_le_n show "x = y" by auto
1.266 +  with a k_le_n show "x = y" by (auto simp add: eq_diff_iff)
1.267  qed
1.268
1.269  text\<open>Rewriting to pull differences out\<close>
1.270
1.271 -lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
1.272 -by arith
1.273 -
1.274 -lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
1.275 -by arith
1.276 -
1.277 -lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
1.278 -by arith
1.279 -
1.280 -lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
1.281 -by simp
1.282 -
1.283 -(*The others are
1.284 -      i - j - k = i - (j + k),
1.285 -      k \<le> j ==> j - k + i = j + i - k,
1.286 -      k \<le> j ==> i + (j - k) = i + j - k *)
1.290 -
1.291 -text\<open>At present we prove no analogue of \<open>not_less_Least\<close> or \<open>Least_Suc\<close>, since there appears to be no need.\<close>
1.292 -
1.293 -text\<open>Lemmas for ex/Factorization\<close>
1.294 -
1.295 -lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
1.296 -by (cases m) auto
1.297 -
1.298 -lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
1.299 -by (cases m) auto
1.300 -
1.301 -lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
1.302 -by (cases m) auto
1.303 +lemma diff_diff_right [simp]:
1.304 +  fixes i j k :: nat
1.305 +  shows "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
1.306 +  by (fact diff_diff_right)
1.307 +
1.308 +lemma diff_Suc_diff_eq1 [simp]:
1.309 +  assumes "k \<le> j"
1.310 +  shows "i - Suc (j - k) = i + k - Suc j"
1.311 +proof -
1.312 +  from assms have *: "Suc (j - k) = Suc j - k"
1.313 +    by (simp add: Suc_diff_le)
1.314 +  from assms have "k \<le> Suc j"
1.315 +    by (rule order_trans) simp
1.316 +  with diff_diff_right [of k "Suc j" i] * show ?thesis
1.317 +    by simp
1.318 +qed
1.319 +
1.320 +lemma diff_Suc_diff_eq2 [simp]:
1.321 +  assumes "k \<le> j"
1.322 +  shows "Suc (j - k) - i = Suc j - (k + i)"
1.323 +proof -
1.324 +  from assms obtain n where "j = k + n"
1.325 +    by (auto dest: le_Suc_ex)
1.326 +  moreover have "Suc n - i = (k + Suc n) - (k + i)"
1.327 +    using add_diff_cancel_left [of k "Suc n" i] by simp
1.328 +  ultimately show ?thesis by simp
1.329 +qed
1.330 +
1.331 +lemma Suc_diff_Suc:
1.332 +  assumes "n < m"
1.333 +  shows "Suc (m - Suc n) = m - n"
1.334 +proof -
1.335 +  from assms obtain q where "m = n + Suc q"
1.336 +    by (auto dest: less_imp_Suc_add)
1.337 +  moreover def r \<equiv> "Suc q"
1.338 +  ultimately have "Suc (m - Suc n) = r" and "m = n + r"
1.339 +    by simp_all
1.340 +  then show ?thesis by simp
1.341 +qed
1.342 +
1.343 +lemma one_less_mult:
1.344 +  "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
1.345 +  using less_1_mult [of n m] by (simp add: ac_simps)
1.346 +
1.347 +lemma n_less_m_mult_n:
1.348 +  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
1.349 +  using mult_strict_right_mono [of 1 m n] by simp
1.350 +
1.351 +lemma n_less_n_mult_m:
1.352 +  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
1.353 +  using mult_strict_left_mono [of 1 m n] by simp
1.354
1.355  text \<open>Specialized induction principles that work "backwards":\<close>
1.356
1.357 -lemma inc_induct[consumes 1, case_names base step]:
1.358 +lemma inc_induct [consumes 1, case_names base step]:
1.359    assumes less: "i \<le> j"
1.360    assumes base: "P j"
1.361    assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
1.362    shows "P i"
1.363    using less step
1.364 -proof (induct d\<equiv>"j - i" arbitrary: i)
1.365 +proof (induct "j - i" arbitrary: i)
1.366    case (0 i)
1.367 -  hence "i = j" by simp
1.368 +  then have "i = j" by simp
1.369    with base show ?case by simp
1.370  next
1.371    case (Suc d n)
1.372 -  hence "n \<le> n" "n < j" "P (Suc n)"
1.373 -    by simp_all
1.374 -  then show "P n" by fact
1.375 +  from Suc.hyps have "n \<noteq> j" by auto
1.376 +  with Suc have "n < j" by (simp add: less_le)
1.377 +  from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
1.378 +  then have "d + 1 - 1 = j - n - 1" by simp
1.379 +  then have "d = j - n - 1" by simp
1.380 +  then have "d = j - (n + 1)"
1.381 +    by (simp add: diff_diff_eq)
1.382 +  then have "d = j - Suc n"
1.383 +    by simp
1.384 +  moreover from \<open>n < j\<close> have "Suc n \<le> j"
1.385 +    by (simp add: Suc_le_eq)
1.386 +  ultimately have "P (Suc n)"
1.387 +  thm Suc.hyps TrueI Suc.prems
1.388 +  proof (rule Suc.hyps)
1.389 +    fix q
1.390 +    assume "Suc n \<le> q"
1.391 +    then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le)
1.392 +    moreover assume "q < j"
1.393 +    moreover assume "P (Suc q)"
1.394 +    ultimately show "P q"
1.395 +      by (rule Suc.prems)
1.396 +  qed
1.397 +  with order_refl \<open>n < j\<close> show "P n"
1.398 +    by (rule Suc.prems)
1.399  qed
1.400 -
1.401 -lemma strict_inc_induct[consumes 1, case_names base step]:
1.402 +
1.403 +lemma strict_inc_induct [consumes 1, case_names base step]:
1.404    assumes less: "i < j"
1.405 -  assumes base: "!!i. j = Suc i ==> P i"
1.406 -  assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
1.407 +  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
1.408 +  assumes step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
1.409    shows "P i"
1.410 -  using less
1.411 -proof (induct d=="j - i - 1" arbitrary: i)
1.412 +using less proof (induct "j - i - 1" arbitrary: i)
1.413    case (0 i)
1.414 -  with \<open>i < j\<close> have "j = Suc i" by simp
1.415 +  from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0"
1.416 +    by (auto dest!: less_imp_Suc_add)
1.417 +  with 0 have "j = Suc i"
1.418 +    by (auto intro: order_antisym simp add: Suc_le_eq)
1.419    with base show ?case by simp
1.420  next
1.421    case (Suc d i)
1.422 -  hence "i < j" "P (Suc i)"
1.423 -    by simp_all
1.424 -  thus "P i" by (rule step)
1.425 +  from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i"
1.427 +  then have "Suc d - 1 = j - Suc i - 1"
1.428 +    by simp
1.429 +  then have "d = j - Suc i - 1"
1.430 +    by simp
1.431 +  moreover from * have "j - Suc i \<noteq> 0"
1.432 +    by auto
1.433 +  then have "Suc i < j"
1.434 +    by (simp add: not_le)
1.435 +  ultimately have "P (Suc i)"
1.436 +    by (rule Suc.hyps)
1.437 +  with \<open>i < j\<close> show "P i" by (rule step)
1.438  qed
1.439
1.440  lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
1.441 @@ -1841,9 +1927,35 @@
1.442
1.443  text \<open>Further induction rule similar to @{thm inc_induct}\<close>
1.444
1.445 -lemma dec_induct[consumes 1, case_names base step]:
1.446 +lemma dec_induct [consumes 1, case_names base step]:
1.447    "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
1.448 -  by (induct j arbitrary: i) (auto simp: le_Suc_eq)
1.449 +proof (induct j arbitrary: i)
1.450 +  case 0 then show ?case by simp
1.451 +next
1.452 +  case (Suc j)
1.453 +  from Suc.prems have "i \<le> j \<or> i = Suc j"
1.454 +    by (simp add: le_Suc_eq)
1.455 +  then show ?case proof
1.456 +    assume "i \<le> j"
1.457 +    moreover have "j < Suc j" by simp
1.458 +    moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
1.459 +    proof (rule Suc.hyps)
1.460 +      fix q
1.461 +      assume "i \<le> q"
1.462 +      moreover assume "q < j" then have "q < Suc j"
1.463 +        by (simp add: less_Suc_eq)
1.464 +      moreover assume "P q"
1.465 +      ultimately show "P (Suc q)"
1.466 +        by (rule Suc.prems)
1.467 +    qed
1.468 +    ultimately show "P (Suc j)"
1.469 +      by (rule Suc.prems)
1.470 +  next
1.471 +    assume "i = Suc j"
1.472 +    with \<open>P i\<close> show "P (Suc j)" by simp
1.473 +  qed
1.474 +qed
1.475 +
1.476
1.477  subsection \<open> Monotonicity of funpow \<close>
1.478
1.479 @@ -1912,7 +2024,7 @@
1.480  proof -
1.481    from assms(1) obtain q where "k * n = (k * m) * q" ..
1.482    then have "k * n = k * (m * q)" by (simp add: ac_simps)
1.483 -  with \<open>0 < k\<close> have "n = m * q" by simp
1.484 +  with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
1.485    then show ?thesis ..
1.486  qed
1.487
1.488 @@ -1949,7 +2061,7 @@
1.489  lemma dvd_minus_self:
1.490    fixes m n :: nat
1.491    shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
1.492 -  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add)
1.493 +  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
1.494