src/HOL/Factorial.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (19 months ago) changeset 67003 49850a679c2c parent 66806 a4e82b58d833 child 67399 eab6ce8368fa permissions -rw-r--r--
more robust sorted_entries;
```     1 (*  Title:      HOL/Factorial.thy
```
```     2     Author:     Jacques D. Fleuriot
```
```     3     Author:     Lawrence C Paulson
```
```     4     Author:     Jeremy Avigad
```
```     5     Author:     Chaitanya Mangla
```
```     6     Author:     Manuel Eberl
```
```     7 *)
```
```     8
```
```     9 section \<open>Factorial Function, Rising Factorials\<close>
```
```    10
```
```    11 theory Factorial
```
```    12   imports Groups_List
```
```    13 begin
```
```    14
```
```    15 subsection \<open>Factorial Function\<close>
```
```    16
```
```    17 context semiring_char_0
```
```    18 begin
```
```    19
```
```    20 definition fact :: "nat \<Rightarrow> 'a"
```
```    21   where fact_prod: "fact n = of_nat (\<Prod>{1..n})"
```
```    22
```
```    23 lemma fact_prod_Suc: "fact n = of_nat (prod Suc {0..<n})"
```
```    24   by (cases n)
```
```    25     (simp_all add: fact_prod prod.atLeast_Suc_atMost_Suc_shift
```
```    26       atLeastLessThanSuc_atLeastAtMost)
```
```    27
```
```    28 lemma fact_prod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
```
```    29   using prod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
```
```    30   by (cases n)
```
```    31     (simp_all add: fact_prod_Suc prod.atLeast_Suc_atMost_Suc_shift
```
```    32       atLeastLessThanSuc_atLeastAtMost)
```
```    33
```
```    34 lemma fact_0 [simp]: "fact 0 = 1"
```
```    35   by (simp add: fact_prod)
```
```    36
```
```    37 lemma fact_1 [simp]: "fact 1 = 1"
```
```    38   by (simp add: fact_prod)
```
```    39
```
```    40 lemma fact_Suc_0 [simp]: "fact (Suc 0) = 1"
```
```    41   by (simp add: fact_prod)
```
```    42
```
```    43 lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
```
```    44   by (simp add: fact_prod atLeastAtMostSuc_conv algebra_simps)
```
```    45
```
```    46 lemma fact_2 [simp]: "fact 2 = 2"
```
```    47   by (simp add: numeral_2_eq_2)
```
```    48
```
```    49 lemma fact_split: "k \<le> n \<Longrightarrow> fact n = of_nat (prod Suc {n - k..<n}) * fact (n - k)"
```
```    50   by (simp add: fact_prod_Suc prod.union_disjoint [symmetric]
```
```    51     ivl_disj_un ac_simps of_nat_mult [symmetric])
```
```    52
```
```    53 end
```
```    54
```
```    55 lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
```
```    56   by (simp add: fact_prod)
```
```    57
```
```    58 lemma of_int_fact [simp]: "of_int (fact n) = fact n"
```
```    59   by (simp only: fact_prod of_int_of_nat_eq)
```
```    60
```
```    61 lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
```
```    62   by (cases n) auto
```
```    63
```
```    64 lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
```
```    65   apply (induct n)
```
```    66   apply auto
```
```    67   using of_nat_eq_0_iff
```
```    68   apply fastforce
```
```    69   done
```
```    70
```
```    71 lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
```
```    72   by (induct n) (auto simp: le_Suc_eq)
```
```    73
```
```    74 lemma fact_in_Nats: "fact n \<in> \<nat>"
```
```    75   by (induct n) auto
```
```    76
```
```    77 lemma fact_in_Ints: "fact n \<in> \<int>"
```
```    78   by (induct n) auto
```
```    79
```
```    80 context
```
```    81   assumes "SORT_CONSTRAINT('a::linordered_semidom)"
```
```    82 begin
```
```    83
```
```    84 lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
```
```    85   by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
```
```    86
```
```    87 lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
```
```    88   by (metis le0 fact_0 fact_mono)
```
```    89
```
```    90 lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
```
```    91   using fact_ge_1 less_le_trans zero_less_one by blast
```
```    92
```
```    93 lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)"
```
```    94   by (simp add: less_imp_le)
```
```    95
```
```    96 lemma fact_not_neg [simp]: "\<not> fact n < (0 :: 'a)"
```
```    97   by (simp add: not_less_iff_gr_or_eq)
```
```    98
```
```    99 lemma fact_le_power: "fact n \<le> (of_nat (n^n) :: 'a)"
```
```   100 proof (induct n)
```
```   101   case 0
```
```   102   then show ?case by simp
```
```   103 next
```
```   104   case (Suc n)
```
```   105   then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)"
```
```   106     by (rule order_trans) (simp add: power_mono del: of_nat_power)
```
```   107   have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"
```
```   108     by (simp add: algebra_simps)
```
```   109   also have "\<dots> \<le> of_nat (Suc n) * of_nat (Suc n ^ n)"
```
```   110     by (simp add: * ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power)
```
```   111   also have "\<dots> \<le> of_nat (Suc n ^ Suc n)"
```
```   112     by (metis of_nat_mult order_refl power_Suc)
```
```   113   finally show ?case .
```
```   114 qed
```
```   115
```
```   116 end
```
```   117
```
```   118 lemma fact_less_mono_nat: "0 < m \<Longrightarrow> m < n \<Longrightarrow> fact m < (fact n :: nat)"
```
```   119   by (induct n) (auto simp: less_Suc_eq)
```
```   120
```
```   121 lemma fact_less_mono: "0 < m \<Longrightarrow> m < n \<Longrightarrow> fact m < (fact n :: 'a::linordered_semidom)"
```
```   122   by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)
```
```   123
```
```   124 lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
```
```   125   by (metis One_nat_def fact_ge_1)
```
```   126
```
```   127 lemma dvd_fact: "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
```
```   128   by (induct n) (auto simp: dvdI le_Suc_eq)
```
```   129
```
```   130 lemma fact_ge_self: "fact n \<ge> n"
```
```   131   by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
```
```   132
```
```   133 lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::linordered_semidom)"
```
```   134   by (induct m) (auto simp: le_Suc_eq)
```
```   135
```
```   136 lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semidom_modulo, linordered_semidom}) = 0"
```
```   137   by (simp add: mod_eq_0_iff_dvd fact_dvd)
```
```   138
```
```   139 lemma fact_div_fact:
```
```   140   assumes "m \<ge> n"
```
```   141   shows "fact m div fact n = \<Prod>{n + 1..m}"
```
```   142 proof -
```
```   143   obtain d where "d = m - n"
```
```   144     by auto
```
```   145   with assms have "m = n + d"
```
```   146     by auto
```
```   147   have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
```
```   148   proof (induct d)
```
```   149     case 0
```
```   150     show ?case by simp
```
```   151   next
```
```   152     case (Suc d')
```
```   153     have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
```
```   154       by simp
```
```   155     also from Suc.hyps have "\<dots> = Suc (n + d') * \<Prod>{n + 1..n + d'}"
```
```   156       unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
```
```   157     also have "\<dots> = \<Prod>{n + 1..n + Suc d'}"
```
```   158       by (simp add: atLeastAtMostSuc_conv)
```
```   159     finally show ?case .
```
```   160   qed
```
```   161   with \<open>m = n + d\<close> show ?thesis by simp
```
```   162 qed
```
```   163
```
```   164 lemma fact_num_eq_if: "fact m = (if m = 0 then 1 else of_nat m * fact (m - 1))"
```
```   165   by (cases m) auto
```
```   166
```
```   167 lemma fact_div_fact_le_pow:
```
```   168   assumes "r \<le> n"
```
```   169   shows "fact n div fact (n - r) \<le> n ^ r"
```
```   170 proof -
```
```   171   have "r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}" for r
```
```   172     by (subst prod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
```
```   173   with assms show ?thesis
```
```   174     by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
```
```   175 qed
```
```   176
```
```   177 lemma fact_numeral: "fact (numeral k) = numeral k * fact (pred_numeral k)"
```
```   178   \<comment> \<open>Evaluation for specific numerals\<close>
```
```   179   by (metis fact_Suc numeral_eq_Suc of_nat_numeral)
```
```   180
```
```   181
```
```   182
```
```   183 subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
```
```   184
```
```   185 text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
```
```   186
```
```   187 context comm_semiring_1
```
```   188 begin
```
```   189
```
```   190 definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
```
```   191   where pochhammer_prod: "pochhammer a n = prod (\<lambda>i. a + of_nat i) {0..<n}"
```
```   192
```
```   193 lemma pochhammer_prod_rev: "pochhammer a n = prod (\<lambda>i. a + of_nat (n - i)) {1..n}"
```
```   194   using prod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
```
```   195   by (simp add: pochhammer_prod)
```
```   196
```
```   197 lemma pochhammer_Suc_prod: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat i) {0..n}"
```
```   198   by (simp add: pochhammer_prod atLeastLessThanSuc_atLeastAtMost)
```
```   199
```
```   200 lemma pochhammer_Suc_prod_rev: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat (n - i)) {0..n}"
```
```   201   by (simp add: pochhammer_prod_rev prod.atLeast_Suc_atMost_Suc_shift)
```
```   202
```
```   203 lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
```
```   204   by (simp add: pochhammer_prod)
```
```   205
```
```   206 lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
```
```   207   by (simp add: pochhammer_prod lessThan_Suc)
```
```   208
```
```   209 lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
```
```   210   by (simp add: pochhammer_prod lessThan_Suc)
```
```   211
```
```   212 lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
```
```   213   by (simp add: pochhammer_prod atLeast0_lessThan_Suc ac_simps)
```
```   214
```
```   215 end
```
```   216
```
```   217 lemma pochhammer_nonneg:
```
```   218   fixes x :: "'a :: linordered_semidom"
```
```   219   shows "x > 0 \<Longrightarrow> pochhammer x n \<ge> 0"
```
```   220   by (induction n) (auto simp: pochhammer_Suc intro!: mult_nonneg_nonneg add_nonneg_nonneg)
```
```   221
```
```   222 lemma pochhammer_pos:
```
```   223   fixes x :: "'a :: linordered_semidom"
```
```   224   shows "x > 0 \<Longrightarrow> pochhammer x n > 0"
```
```   225   by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)
```
```   226
```
```   227 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
```
```   228   by (simp add: pochhammer_prod)
```
```   229
```
```   230 lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
```
```   231   by (simp add: pochhammer_prod)
```
```   232
```
```   233 lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
```
```   234   by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps)
```
```   235
```
```   236 lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
```
```   237   by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc ac_simps)
```
```   238
```
```   239 lemma pochhammer_fact: "fact n = pochhammer 1 n"
```
```   240   by (simp add: pochhammer_prod fact_prod_Suc)
```
```   241
```
```   242 lemma pochhammer_of_nat_eq_0_lemma: "k > n \<Longrightarrow> pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
```
```   243   by (auto simp add: pochhammer_prod)
```
```   244
```
```   245 lemma pochhammer_of_nat_eq_0_lemma':
```
```   246   assumes kn: "k \<le> n"
```
```   247   shows "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k \<noteq> 0"
```
```   248 proof (cases k)
```
```   249   case 0
```
```   250   then show ?thesis by simp
```
```   251 next
```
```   252   case (Suc h)
```
```   253   then show ?thesis
```
```   254     apply (simp add: pochhammer_Suc_prod)
```
```   255     using Suc kn
```
```   256     apply (auto simp add: algebra_simps)
```
```   257     done
```
```   258 qed
```
```   259
```
```   260 lemma pochhammer_of_nat_eq_0_iff:
```
```   261   "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
```
```   262   (is "?l = ?r")
```
```   263   using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
```
```   264     pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
```
```   265   by (auto simp add: not_le[symmetric])
```
```   266
```
```   267 lemma pochhammer_0_left:
```
```   268   "pochhammer 0 n = (if n = 0 then 1 else 0)"
```
```   269   by (induction n) (simp_all add: pochhammer_rec)
```
```   270
```
```   271 lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
```
```   272   by (auto simp add: pochhammer_prod eq_neg_iff_add_eq_0)
```
```   273
```
```   274 lemma pochhammer_eq_0_mono:
```
```   275   "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
```
```   276   unfolding pochhammer_eq_0_iff by auto
```
```   277
```
```   278 lemma pochhammer_neq_0_mono:
```
```   279   "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
```
```   280   unfolding pochhammer_eq_0_iff by auto
```
```   281
```
```   282 lemma pochhammer_minus:
```
```   283   "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
```
```   284 proof (cases k)
```
```   285   case 0
```
```   286   then show ?thesis by simp
```
```   287 next
```
```   288   case (Suc h)
```
```   289   have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)"
```
```   290     using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
```
```   291     by auto
```
```   292   with Suc show ?thesis
```
```   293     using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
```
```   294     by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff)
```
```   295 qed
```
```   296
```
```   297 lemma pochhammer_minus':
```
```   298   "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
```
```   299   apply (simp only: pochhammer_minus [where b = b])
```
```   300   apply (simp only: mult.assoc [symmetric])
```
```   301   apply (simp only: power_add [symmetric])
```
```   302   apply simp
```
```   303   done
```
```   304
```
```   305 lemma pochhammer_same: "pochhammer (- of_nat n) n =
```
```   306     ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n"
```
```   307   unfolding pochhammer_minus
```
```   308   by (simp add: of_nat_diff pochhammer_fact)
```
```   309
```
```   310 lemma pochhammer_product': "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
```
```   311 proof (induct n arbitrary: z)
```
```   312   case 0
```
```   313   then show ?case by simp
```
```   314 next
```
```   315   case (Suc n z)
```
```   316   have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =
```
```   317       z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
```
```   318     by (simp add: pochhammer_rec ac_simps)
```
```   319   also note Suc[symmetric]
```
```   320   also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))"
```
```   321     by (subst pochhammer_rec) simp
```
```   322   finally show ?case
```
```   323     by simp
```
```   324 qed
```
```   325
```
```   326 lemma pochhammer_product:
```
```   327   "m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
```
```   328   using pochhammer_product'[of z m "n - m"] by simp
```
```   329
```
```   330 lemma pochhammer_times_pochhammer_half:
```
```   331   fixes z :: "'a::field_char_0"
```
```   332   shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
```
```   333 proof (induct n)
```
```   334   case 0
```
```   335   then show ?case
```
```   336     by (simp add: atLeast0_atMost_Suc)
```
```   337 next
```
```   338   case (Suc n)
```
```   339   define n' where "n' = Suc n"
```
```   340   have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =
```
```   341       (pochhammer z n' * pochhammer (z + 1 / 2) n') * ((z + of_nat n') * (z + 1/2 + of_nat n'))"
```
```   342     (is "_ = _ * ?A")
```
```   343     by (simp_all add: pochhammer_rec' mult_ac)
```
```   344   also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
```
```   345     (is "_ = ?B")
```
```   346     by (simp add: field_simps n'_def)
```
```   347   also note Suc[folded n'_def]
```
```   348   also have "(\<Prod>k=0..2 * n + 1. z + of_nat k / 2) * ?B = (\<Prod>k=0..2 * Suc n + 1. z + of_nat k / 2)"
```
```   349     by (simp add: atLeast0_atMost_Suc)
```
```   350   finally show ?case
```
```   351     by (simp add: n'_def)
```
```   352 qed
```
```   353
```
```   354 lemma pochhammer_double:
```
```   355   fixes z :: "'a::field_char_0"
```
```   356   shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"
```
```   357 proof (induct n)
```
```   358   case 0
```
```   359   then show ?case by simp
```
```   360 next
```
```   361   case (Suc n)
```
```   362   have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *
```
```   363       (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"
```
```   364     by (simp add: pochhammer_rec' ac_simps)
```
```   365   also note Suc
```
```   366   also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *
```
```   367         (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
```
```   368       of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
```
```   369     by (simp add: field_simps pochhammer_rec')
```
```   370   finally show ?case .
```
```   371 qed
```
```   372
```
```   373 lemma fact_double:
```
```   374   "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a::field_char_0)"
```
```   375   using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact)
```
```   376
```
```   377 lemma pochhammer_absorb_comp: "(r - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
```
```   378   (is "?lhs = ?rhs")
```
```   379   for r :: "'a::comm_ring_1"
```
```   380 proof -
```
```   381   have "?lhs = - pochhammer (- r) (Suc k)"
```
```   382     by (subst pochhammer_rec') (simp add: algebra_simps)
```
```   383   also have "\<dots> = ?rhs"
```
```   384     by (subst pochhammer_rec) simp
```
```   385   finally show ?thesis .
```
```   386 qed
```
```   387
```
```   388
```
```   389 subsection \<open>Misc\<close>
```
```   390
```
```   391 lemma fact_code [code]:
```
```   392   "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a::semiring_char_0)"
```
```   393 proof -
```
```   394   have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
```
```   395     by (simp add: fact_prod)
```
```   396   also have "\<Prod>{1..n} = \<Prod>{2..n}"
```
```   397     by (intro prod.mono_neutral_right) auto
```
```   398   also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
```
```   399     by (simp add: prod_atLeastAtMost_code)
```
```   400   finally show ?thesis .
```
```   401 qed
```
```   402
```
```   403 lemma pochhammer_code [code]:
```
```   404   "pochhammer a n =
```
```   405     (if n = 0 then 1
```
```   406      else fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
```
```   407   by (cases n)
```
```   408     (simp_all add: pochhammer_prod prod_atLeastAtMost_code [symmetric]
```
```   409       atLeastLessThanSuc_atLeastAtMost)
```
```   410
```
```   411 end
```