Documentation

Init.Data.Nat.Basic

@[reducible, inline]
abbrev Nat.recAux {motive : NatSort u} (zero : motive 0) (succ : (n : Nat) → motive nmotive (n + 1)) (t : Nat) :
motive t

A recursor for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

It is otherwise identical to the default recursor Nat.rec. It is used by the induction tactic by default for Nat.

Equations
    Instances For
      @[reducible, inline]
      abbrev Nat.casesAuxOn {motive : NatSort u} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) :
      motive t

      A case analysis principle for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

      It is otherwise identical to the default recursor Nat.casesOn. It is used as the default Nat case analysis principle for Nat by the cases tactic.

      Equations
        Instances For
          @[specialize #[]]
          def Nat.repeat {α : Type u} (f : αα) (n : Nat) (a : α) :
          α

          Applies a function to a starting value the specified number of times.

          In other words, f is iterated n times on a.

          Examples:

          Equations
            Instances For
              @[inline]
              def Nat.repeatTR {α : Type u} (f : αα) (n : Nat) (a : α) :
              α

              Applies a function to a starting value the specified number of times.

              In other words, f is iterated n times on a.

              This is a tail-recursive version of Nat.repeat that's used at runtime.

              Examples:

              Equations
                Instances For
                  @[specialize #[]]
                  def Nat.repeatTR.loop {α : Type u} (f : αα) :
                  Natαα
                  Equations
                    Instances For
                      def Nat.blt (a b : Nat) :

                      The Boolean less-than comparison on natural numbers.

                      This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

                      Examples:

                      Equations
                        Instances For
                          theorem Nat.and_forall_add_one {p : NatProp} :
                          (p 0 ∀ (n : Nat), p (n + 1)) ∀ (n : Nat), p n
                          theorem Nat.or_exists_add_one {p : NatProp} :
                          (p 0 (n : Nat), p (n + 1)) Exists p

                          Helper "packing" theorems #

                          @[simp]
                          theorem Nat.zero_eq :
                          @[simp]
                          theorem Nat.add_eq {x y : Nat} :
                          x.add y = x + y
                          @[simp]
                          theorem Nat.mul_eq {x y : Nat} :
                          x.mul y = x * y
                          @[simp]
                          theorem Nat.sub_eq {x y : Nat} :
                          x.sub y = x - y
                          @[simp]
                          theorem Nat.lt_eq {x y : Nat} :
                          x.lt y = (x < y)
                          @[simp]
                          theorem Nat.le_eq {x y : Nat} :
                          x.le y = (x y)

                          Helper Bool relation theorems #

                          @[simp]
                          theorem Nat.beq_refl (a : Nat) :
                          a.beq a = true
                          @[simp]
                          theorem Nat.beq_eq {x y : Nat} :
                          (x.beq y = true) = (x = y)
                          @[simp]
                          theorem Nat.ble_eq {x y : Nat} :
                          (x.ble y = true) = (x y)
                          @[simp]
                          theorem Nat.blt_eq {x y : Nat} :
                          (x.blt y = true) = (x < y)
                          theorem Nat.beq_eq_true_eq (a b : Nat) :
                          ((a == b) = true) = (a = b)
                          theorem Nat.not_beq_eq_true_eq (a b : Nat) :
                          ((!a == b) = true) = ¬a = b

                          Nat.add theorems #

                          @[simp]
                          theorem Nat.zero_add (n : Nat) :
                          0 + n = n
                          instance Nat.instLawfulIdentityHAddOfNat :
                          Std.LawfulIdentity (fun (x1 x2 : Nat) => x1 + x2) 0
                          theorem Nat.succ_add (n m : Nat) :
                          n.succ + m = (n + m).succ
                          theorem Nat.add_succ (n m : Nat) :
                          n + m.succ = (n + m).succ
                          theorem Nat.add_one (n : Nat) :
                          n + 1 = n.succ
                          @[simp]
                          theorem Nat.succ_eq_add_one (n : Nat) :
                          n.succ = n + 1
                          theorem Nat.add_one_ne_zero (n : Nat) :
                          n + 1 0
                          theorem Nat.zero_ne_add_one (n : Nat) :
                          0 n + 1
                          theorem Nat.add_comm (n m : Nat) :
                          n + m = m + n
                          instance Nat.instCommutativeHAdd :
                          Std.Commutative fun (x1 x2 : Nat) => x1 + x2
                          theorem Nat.add_assoc (n m k : Nat) :
                          n + m + k = n + (m + k)
                          instance Nat.instAssociativeHAdd :
                          Std.Associative fun (x1 x2 : Nat) => x1 + x2
                          theorem Nat.add_left_comm (n m k : Nat) :
                          n + (m + k) = m + (n + k)
                          theorem Nat.add_right_comm (n m k : Nat) :
                          n + m + k = n + k + m
                          theorem Nat.add_left_cancel {n m k : Nat} :
                          n + m = n + km = k
                          theorem Nat.add_right_cancel {n m k : Nat} (h : n + m = k + m) :
                          n = k
                          theorem Nat.eq_zero_of_add_eq_zero {n m : Nat} :
                          n + m = 0n = 0 m = 0
                          theorem Nat.eq_zero_of_add_eq_zero_left {n m : Nat} (h : n + m = 0) :
                          m = 0

                          Nat.mul theorems #

                          @[simp]
                          theorem Nat.mul_zero (n : Nat) :
                          n * 0 = 0
                          theorem Nat.mul_succ (n m : Nat) :
                          n * m.succ = n * m + n
                          theorem Nat.mul_add_one (n m : Nat) :
                          n * (m + 1) = n * m + n
                          @[simp]
                          theorem Nat.zero_mul (n : Nat) :
                          0 * n = 0
                          theorem Nat.succ_mul (n m : Nat) :
                          n.succ * m = n * m + m
                          theorem Nat.add_one_mul (n m : Nat) :
                          (n + 1) * m = n * m + m
                          theorem Nat.mul_comm (n m : Nat) :
                          n * m = m * n
                          instance Nat.instCommutativeHMul :
                          Std.Commutative fun (x1 x2 : Nat) => x1 * x2
                          @[simp]
                          theorem Nat.mul_one (n : Nat) :
                          n * 1 = n
                          @[simp]
                          theorem Nat.one_mul (n : Nat) :
                          1 * n = n
                          instance Nat.instLawfulIdentityHMulOfNat :
                          Std.LawfulIdentity (fun (x1 x2 : Nat) => x1 * x2) 1
                          theorem Nat.left_distrib (n m k : Nat) :
                          n * (m + k) = n * m + n * k
                          theorem Nat.right_distrib (n m k : Nat) :
                          (n + m) * k = n * k + m * k
                          theorem Nat.mul_add (n m k : Nat) :
                          n * (m + k) = n * m + n * k
                          theorem Nat.add_mul (n m k : Nat) :
                          (n + m) * k = n * k + m * k
                          theorem Nat.mul_assoc (n m k : Nat) :
                          n * m * k = n * (m * k)
                          instance Nat.instAssociativeHMul :
                          Std.Associative fun (x1 x2 : Nat) => x1 * x2
                          theorem Nat.mul_left_comm (n m k : Nat) :
                          n * (m * k) = m * (n * k)
                          theorem Nat.mul_two (n : Nat) :
                          n * 2 = n + n
                          theorem Nat.two_mul (n : Nat) :
                          2 * n = n + n

                          Inequalities #

                          theorem Nat.succ_lt_succ {n m : Nat} :
                          n < mn.succ < m.succ
                          theorem Nat.lt_succ_of_le {n m : Nat} :
                          n mn < m.succ
                          theorem Nat.le_of_lt_add_one {n m : Nat} :
                          n < m + 1n m
                          theorem Nat.lt_add_one_of_le {n m : Nat} :
                          n mn < m + 1
                          @[simp]
                          theorem Nat.sub_zero (n : Nat) :
                          n - 0 = n
                          theorem Nat.add_one_pos (n : Nat) :
                          0 < n + 1
                          theorem Nat.succ_sub_succ_eq_sub (n m : Nat) :
                          n.succ - m.succ = n - m
                          theorem Nat.pred_le (n : Nat) :
                          n.pred n
                          theorem Nat.pred_lt {n : Nat} :
                          n 0n.pred < n
                          theorem Nat.sub_one_lt {n : Nat} :
                          n 0n - 1 < n
                          @[simp]
                          theorem Nat.sub_le (n m : Nat) :
                          n - m n
                          theorem Nat.sub_lt_of_lt {a b c : Nat} (h : a < c) :
                          a - b < c
                          theorem Nat.sub_lt {n m : Nat} :
                          0 < n0 < mn - m < n
                          theorem Nat.sub_succ (n m : Nat) :
                          n - m.succ = (n - m).pred
                          theorem Nat.succ_sub_succ (n m : Nat) :
                          n.succ - m.succ = n - m
                          @[simp]
                          theorem Nat.sub_self (n : Nat) :
                          n - n = 0
                          theorem Nat.sub_add_eq (a b c : Nat) :
                          a - (b + c) = a - b - c
                          theorem Nat.lt_of_lt_of_le {n m k : Nat} :
                          n < mm kn < k
                          theorem Nat.lt_of_lt_of_eq {n m k : Nat} :
                          n < mm = kn < k
                          instance Nat.instTransLt :
                          Trans (fun (x1 x2 : Nat) => x1 < x2) (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 < x2
                          Equations
                            instance Nat.instTransLe :
                            Trans (fun (x1 x2 : Nat) => x1 x2) (fun (x1 x2 : Nat) => x1 x2) fun (x1 x2 : Nat) => x1 x2
                            Equations
                              instance Nat.instTransLtLe :
                              Trans (fun (x1 x2 : Nat) => x1 < x2) (fun (x1 x2 : Nat) => x1 x2) fun (x1 x2 : Nat) => x1 < x2
                              Equations
                                instance Nat.instTransLeLt :
                                Trans (fun (x1 x2 : Nat) => x1 x2) (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 < x2
                                Equations
                                  theorem Nat.le_of_eq {n m : Nat} (p : n = m) :
                                  n m
                                  theorem Nat.lt.step {n m : Nat} :
                                  n < mn < m.succ
                                  theorem Nat.le_of_succ_le {n m : Nat} (h : n.succ m) :
                                  n m
                                  theorem Nat.lt_of_succ_lt {n m : Nat} :
                                  n.succ < mn < m
                                  theorem Nat.le_of_lt {n m : Nat} :
                                  n < mn m
                                  theorem Nat.lt_of_succ_lt_succ {n m : Nat} :
                                  n.succ < m.succn < m
                                  theorem Nat.lt_of_succ_le {n m : Nat} (h : n.succ m) :
                                  n < m
                                  theorem Nat.succ_le_of_lt {n m : Nat} (h : n < m) :
                                  n.succ m
                                  theorem Nat.eq_zero_or_pos (n : Nat) :
                                  n = 0 n > 0
                                  theorem Nat.pos_of_ne_zero {n : Nat} :
                                  n 00 < n
                                  theorem Nat.pos_of_neZero (n : Nat) [NeZero n] :
                                  0 < n
                                  theorem Nat.lt.base (n : Nat) :
                                  n < n.succ
                                  theorem Nat.lt_succ_self (n : Nat) :
                                  n < n.succ
                                  @[simp]
                                  theorem Nat.lt_add_one (n : Nat) :
                                  n < n + 1
                                  theorem Nat.le_total (m n : Nat) :
                                  m n n m
                                  theorem Nat.eq_zero_of_le_zero {n : Nat} (h : n 0) :
                                  n = 0
                                  theorem Nat.zero_lt_of_lt {a b : Nat} :
                                  a < b0 < b
                                  theorem Nat.zero_lt_of_ne_zero {a : Nat} (h : a 0) :
                                  0 < a
                                  theorem Nat.ne_of_lt {a b : Nat} (h : a < b) :
                                  a b
                                  theorem Nat.le_or_eq_of_le_succ {m n : Nat} (h : m n.succ) :
                                  m n m = n.succ
                                  theorem Nat.le_or_eq_of_le_add_one {m n : Nat} (h : m n + 1) :
                                  m n m = n + 1
                                  @[simp]
                                  theorem Nat.le_add_right (n k : Nat) :
                                  n n + k
                                  @[simp]
                                  theorem Nat.le_add_left (n m : Nat) :
                                  n m + n
                                  theorem Nat.le_of_add_right_le {n m k : Nat} (h : n + k m) :
                                  n m
                                  theorem Nat.le_add_right_of_le {n m k : Nat} (h : n m) :
                                  n m + k
                                  theorem Nat.lt_of_add_one_le {n m : Nat} (h : n + 1 m) :
                                  n < m
                                  theorem Nat.add_one_le_of_lt {n m : Nat} (h : n < m) :
                                  n + 1 m
                                  theorem Nat.lt_add_left {a b : Nat} (c : Nat) (h : a < b) :
                                  a < c + b
                                  theorem Nat.lt_add_right {a b : Nat} (c : Nat) (h : a < b) :
                                  a < b + c
                                  theorem Nat.lt_of_add_right_lt {n m k : Nat} (h : n + k < m) :
                                  n < m
                                  theorem Nat.lt_of_add_left_lt {n m k : Nat} (h : k + n < m) :
                                  n < m
                                  theorem Nat.le.dest {n m : Nat} :
                                  n m (k : Nat), n + k = m
                                  theorem Nat.le.intro {n m k : Nat} (h : n + k = m) :
                                  n m
                                  theorem Nat.not_le_of_gt {n m : Nat} (h : n > m) :
                                  ¬n m
                                  theorem Nat.not_le_of_lt {a b : Nat} :
                                  a < b¬b a
                                  theorem Nat.not_lt_of_ge {a b : Nat} :
                                  b a¬b < a
                                  theorem Nat.not_lt_of_le {a b : Nat} :
                                  a b¬b < a
                                  theorem Nat.lt_le_asymm {a b : Nat} :
                                  a < b¬b a
                                  theorem Nat.le_lt_asymm {a b : Nat} :
                                  a b¬b < a
                                  theorem Nat.gt_of_not_le {n m : Nat} (h : ¬n m) :
                                  n > m
                                  theorem Nat.lt_of_not_ge {a b : Nat} :
                                  ¬b ab < a
                                  theorem Nat.lt_of_not_le {a b : Nat} :
                                  ¬a bb < a
                                  theorem Nat.ge_of_not_lt {n m : Nat} (h : ¬n < m) :
                                  n m
                                  theorem Nat.le_of_not_gt {a b : Nat} :
                                  ¬b > ab a
                                  theorem Nat.le_of_not_lt {a b : Nat} :
                                  ¬a < bb a
                                  theorem Nat.ne_of_gt {a b : Nat} (h : b < a) :
                                  a b
                                  theorem Nat.ne_of_lt' {a b : Nat} :
                                  a < bb a
                                  @[simp]
                                  theorem Nat.not_le {a b : Nat} :
                                  ¬a b b < a
                                  @[simp]
                                  theorem Nat.not_lt {a b : Nat} :
                                  ¬a < b b a
                                  theorem Nat.le_of_not_le {a b : Nat} (h : ¬b a) :
                                  a b
                                  theorem Nat.le_of_not_ge {a b : Nat} :
                                  ¬a ba b
                                  theorem Nat.lt_trichotomy (a b : Nat) :
                                  a < b a = b b < a
                                  theorem Nat.lt_or_gt_of_ne {a b : Nat} (ne : a b) :
                                  a < b a > b
                                  theorem Nat.lt_or_lt_of_ne {a b : Nat} :
                                  a ba < b b < a
                                  theorem Nat.le_antisymm_iff {a b : Nat} :
                                  a = b a b b a
                                  theorem Nat.eq_iff_le_and_ge {a b : Nat} :
                                  a = b a b b a
                                  instance Nat.instAntisymmLe :
                                  Std.Antisymm fun (x1 x2 : Nat) => x1 x2
                                  instance Nat.instAntisymmNotLt :
                                  Std.Antisymm fun (x1 x2 : Nat) => ¬x1 < x2
                                  theorem Nat.add_le_add_left {n m : Nat} (h : n m) (k : Nat) :
                                  k + n k + m
                                  theorem Nat.add_le_add_right {n m : Nat} (h : n m) (k : Nat) :
                                  n + k m + k
                                  theorem Nat.add_lt_add_left {n m : Nat} (h : n < m) (k : Nat) :
                                  k + n < k + m
                                  theorem Nat.add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) :
                                  n + k < m + k
                                  theorem Nat.lt_add_of_pos_left {k n : Nat} (h : 0 < k) :
                                  n < k + n
                                  theorem Nat.lt_add_of_pos_right {k n : Nat} (h : 0 < k) :
                                  n < n + k
                                  theorem Nat.pos_iff_ne_zero {n : Nat} :
                                  0 < n n 0
                                  theorem Nat.add_le_add {a b c d : Nat} (h₁ : a b) (h₂ : c d) :
                                  a + c b + d
                                  theorem Nat.add_lt_add {a b c d : Nat} (h₁ : a < b) (h₂ : c < d) :
                                  a + c < b + d
                                  theorem Nat.le_of_add_le_add_left {a b c : Nat} (h : a + b a + c) :
                                  b c
                                  theorem Nat.le_of_add_le_add_right {a b c : Nat} :
                                  a + b c + ba c
                                  @[simp]
                                  theorem Nat.add_le_add_iff_right {m k n : Nat} :
                                  m + n k + n m k
                                  @[simp]
                                  theorem Nat.add_le_add_iff_left {m k n : Nat} :
                                  n + m n + k m k

                                  le/lt #

                                  theorem Nat.lt_asymm {a b : Nat} (h : a < b) :
                                  ¬b < a
                                  @[reducible, inline]
                                  abbrev Nat.not_lt_of_gt {a b : Nat} (h : a < b) :
                                  ¬b < a

                                  Alias for Nat.lt_asymm.

                                  Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev Nat.not_lt_of_lt {a b : Nat} (h : a < b) :
                                      ¬b < a

                                      Alias for Nat.lt_asymm.

                                      Equations
                                        Instances For
                                          theorem Nat.lt_iff_le_not_le {m n : Nat} :
                                          m < n m n ¬n m
                                          @[reducible, inline]
                                          abbrev Nat.lt_iff_le_and_not_ge {m n : Nat} :
                                          m < n m n ¬n m

                                          Alias for Nat.lt_iff_le_not_le.

                                          Equations
                                            Instances For
                                              theorem Nat.lt_iff_le_and_ne {m n : Nat} :
                                              m < n m n m n
                                              theorem Nat.ne_iff_lt_or_gt {a b : Nat} :
                                              a b a < b b < a
                                              @[reducible, inline]
                                              abbrev Nat.lt_or_gt {a b : Nat} :
                                              a b a < b b < a

                                              Alias for Nat.ne_iff_lt_or_gt.

                                              Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev Nat.le_or_ge (m n : Nat) :
                                                  m n n m

                                                  Alias for Nat.le_total.

                                                  Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev Nat.le_or_le (m n : Nat) :
                                                      m n n m

                                                      Alias for Nat.le_total.

                                                      Equations
                                                        Instances For
                                                          theorem Nat.eq_or_lt_of_not_lt {a b : Nat} (hnlt : ¬a < b) :
                                                          a = b b < a
                                                          theorem Nat.lt_or_eq_of_le {n m : Nat} (h : n m) :
                                                          n < m n = m
                                                          theorem Nat.le_iff_lt_or_eq {n m : Nat} :
                                                          n m n < m n = m
                                                          theorem Nat.lt_succ_iff {m n : Nat} :
                                                          m < n.succ m n
                                                          theorem Nat.lt_add_one_iff {m n : Nat} :
                                                          m < n + 1 m n
                                                          theorem Nat.lt_succ_iff_lt_or_eq {m n : Nat} :
                                                          m < n.succ m < n m = n
                                                          theorem Nat.lt_add_one_iff_lt_or_eq {m n : Nat} :
                                                          m < n + 1 m < n m = n
                                                          theorem Nat.eq_of_lt_succ_of_not_lt {m n : Nat} (hmn : m < n + 1) (h : ¬m < n) :
                                                          m = n
                                                          theorem Nat.eq_of_le_of_lt_succ {n m : Nat} (h₁ : n m) (h₂ : m < n + 1) :
                                                          m = n

                                                          zero/one/two #

                                                          theorem Nat.le_zero {i : Nat} :
                                                          i 0 i = 0
                                                          @[reducible, inline]
                                                          abbrev Nat.one_pos :
                                                          0 < 1

                                                          Alias for Nat.zero_lt_one.

                                                          Equations
                                                            Instances For
                                                              theorem Nat.two_pos :
                                                              0 < 2
                                                              theorem Nat.ne_zero_iff_zero_lt {n : Nat} :
                                                              n 0 0 < n
                                                              theorem Nat.one_lt_two :
                                                              1 < 2
                                                              theorem Nat.eq_zero_of_not_pos {n : Nat} (h : ¬0 < n) :
                                                              n = 0

                                                              succ/pred #

                                                              @[simp]
                                                              theorem Nat.succ_ne_self (n : Nat) :
                                                              n.succ n
                                                              theorem Nat.add_one_ne_self (n : Nat) :
                                                              n + 1 n
                                                              theorem Nat.succ_le {n m : Nat} :
                                                              n.succ m n < m
                                                              theorem Nat.add_one_le_iff {n m : Nat} :
                                                              n + 1 m n < m
                                                              theorem Nat.lt_succ {m n : Nat} :
                                                              m < n.succ m n
                                                              theorem Nat.lt_succ_of_lt {a b : Nat} (h : a < b) :
                                                              a < b.succ
                                                              theorem Nat.lt_add_one_of_lt {a b : Nat} (h : a < b) :
                                                              a < b + 1
                                                              @[simp]
                                                              theorem Nat.lt_one_iff {n : Nat} :
                                                              n < 1 n = 0
                                                              theorem Nat.succ_pred_eq_of_ne_zero {n : Nat} :
                                                              n 0n.pred.succ = n
                                                              theorem Nat.succ_inj {a b : Nat} :
                                                              a.succ = b.succ a = b
                                                              @[deprecated Nat.succ_inj (since := "2025-04-14")]
                                                              theorem Nat.succ_inj' {a b : Nat} :
                                                              a.succ = b.succ a = b
                                                              theorem Nat.succ_le_succ_iff {a b : Nat} :
                                                              a.succ b.succ a b
                                                              theorem Nat.succ_lt_succ_iff {a b : Nat} :
                                                              a.succ < b.succ a < b
                                                              theorem Nat.succ_ne_succ_iff {a b : Nat} :
                                                              a.succ b.succ a b
                                                              theorem Nat.add_one_inj {a b : Nat} :
                                                              a + 1 = b + 1 a = b
                                                              theorem Nat.ne_add_one (n : Nat) :
                                                              n n + 1
                                                              theorem Nat.add_one_ne (n : Nat) :
                                                              n + 1 n
                                                              theorem Nat.add_one_le_add_one_iff {a b : Nat} :
                                                              a + 1 b + 1 a b
                                                              theorem Nat.add_one_lt_add_one_iff {a b : Nat} :
                                                              a + 1 < b + 1 a < b
                                                              theorem Nat.add_one_ne_add_one_iff {a b : Nat} :
                                                              a + 1 b + 1 a b
                                                              theorem Nat.add_one_add_one_ne_one {a : Nat} :
                                                              a + 1 + 1 1
                                                              theorem Nat.pred_inj {a b : Nat} :
                                                              0 < a0 < ba.pred = b.preda = b
                                                              theorem Nat.pred_ne_self {a : Nat} :
                                                              a 0a.pred a
                                                              theorem Nat.sub_one_ne_self {a : Nat} :
                                                              a 0a - 1 a
                                                              theorem Nat.pred_lt_self {a : Nat} :
                                                              0 < aa.pred < a
                                                              theorem Nat.pred_lt_pred {n m : Nat} :
                                                              n 0n < mn.pred < m.pred
                                                              theorem Nat.pred_le_iff_le_succ {n : Nat} {m : Nat} :
                                                              n.pred m n m.succ
                                                              theorem Nat.le_succ_of_pred_le {n : Nat} {m : Nat} :
                                                              n.pred mn m.succ
                                                              theorem Nat.pred_le_of_le_succ {n m : Nat} :
                                                              n m.succn.pred m
                                                              theorem Nat.lt_pred_iff_succ_lt {n : Nat} {m : Nat} :
                                                              n < m.pred n.succ < m
                                                              theorem Nat.succ_lt_of_lt_pred {n : Nat} {m : Nat} :
                                                              n < m.predn.succ < m
                                                              theorem Nat.lt_pred_of_succ_lt {n m : Nat} :
                                                              n.succ < mn < m.pred
                                                              theorem Nat.le_pred_iff_lt {n : Nat} {m : Nat} :
                                                              0 < m → (n m.pred n < m)
                                                              theorem Nat.le_pred_of_lt {n m : Nat} (h : n < m) :
                                                              n m.pred
                                                              theorem Nat.le_sub_one_of_lt {a b : Nat} :
                                                              a < ba b - 1
                                                              theorem Nat.lt_of_le_pred {m : Nat} {n : Nat} (h : 0 < m) :
                                                              n m.predn < m
                                                              theorem Nat.lt_of_le_sub_one {m n : Nat} (h : 0 < m) :
                                                              n m - 1n < m
                                                              theorem Nat.le_sub_one_iff_lt {m n : Nat} (h : 0 < m) :
                                                              n m - 1 n < m
                                                              theorem Nat.exists_eq_add_one_of_ne_zero {n : Nat} :
                                                              n 0 (k : Nat), n = k + 1

                                                              Basic theorems for comparing numerals #

                                                              @[simp]
                                                              theorem Nat.zero_ne_one :
                                                              0 1
                                                              theorem Nat.succ_ne_zero (n : Nat) :
                                                              n.succ 0
                                                              instance Nat.instNeZeroSucc {n : Nat} :
                                                              NeZero (n + 1)

                                                              mul + order #

                                                              theorem Nat.mul_le_mul_left {n m : Nat} (k : Nat) (h : n m) :
                                                              k * n k * m
                                                              theorem Nat.mul_le_mul_right {n m : Nat} (k : Nat) (h : n m) :
                                                              n * k m * k
                                                              theorem Nat.mul_le_mul {n₁ m₁ n₂ m₂ : Nat} (h₁ : n₁ n₂) (h₂ : m₁ m₂) :
                                                              n₁ * m₁ n₂ * m₂
                                                              theorem Nat.mul_lt_mul_of_pos_left {n m k : Nat} (h : n < m) (hk : k > 0) :
                                                              k * n < k * m
                                                              theorem Nat.mul_lt_mul_of_pos_right {n m k : Nat} (h : n < m) (hk : k > 0) :
                                                              n * k < m * k
                                                              theorem Nat.mul_pos {n m : Nat} (ha : n > 0) (hb : m > 0) :
                                                              n * m > 0
                                                              theorem Nat.le_of_mul_le_mul_left {a b c : Nat} (h : c * a c * b) (hc : 0 < c) :
                                                              a b
                                                              theorem Nat.le_of_mul_le_mul_right {a b c : Nat} (h : a * c b * c) (hc : 0 < c) :
                                                              a b
                                                              theorem Nat.mul_le_mul_left_iff {n m k : Nat} (w : 0 < k) :
                                                              k * n k * m n m
                                                              theorem Nat.mul_le_mul_right_iff {n m k : Nat} (w : 0 < k) :
                                                              n * k m * k n m
                                                              theorem Nat.eq_of_mul_eq_mul_left {m k n : Nat} (hn : 0 < n) (h : n * m = n * k) :
                                                              m = k
                                                              theorem Nat.eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) :
                                                              n = k

                                                              power #

                                                              theorem Nat.pow_succ (n m : Nat) :
                                                              n ^ m.succ = n ^ m * n
                                                              theorem Nat.pow_add_one (n m : Nat) :
                                                              n ^ (m + 1) = n ^ m * n
                                                              @[simp]
                                                              theorem Nat.pow_zero (n : Nat) :
                                                              n ^ 0 = 1
                                                              @[simp]
                                                              theorem Nat.pow_one (a : Nat) :
                                                              a ^ 1 = a
                                                              theorem Nat.pow_le_pow_left {n m : Nat} (h : n m) (i : Nat) :
                                                              n ^ i m ^ i
                                                              theorem Nat.pow_le_pow_right {n : Nat} (hx : n > 0) {i j : Nat} :
                                                              i jn ^ i n ^ j
                                                              @[reducible, inline, deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
                                                              abbrev Nat.pow_le_pow_of_le_left {n m : Nat} (h : n m) (i : Nat) :
                                                              n ^ i m ^ i
                                                              Equations
                                                                Instances For
                                                                  @[reducible, inline, deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
                                                                  abbrev Nat.pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i j : Nat} :
                                                                  i jn ^ i n ^ j
                                                                  Equations
                                                                    Instances For
                                                                      theorem Nat.pow_pos {a n : Nat} (h : 0 < a) :
                                                                      0 < a ^ n
                                                                      @[reducible, inline, deprecated Nat.pow_pos (since := "2025-02-17")]
                                                                      abbrev Nat.pos_pow_of_pos {a n : Nat} (h : 0 < a) :
                                                                      0 < a ^ n
                                                                      Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Nat.zero_pow_of_pos (n : Nat) (h : 0 < n) :
                                                                          0 ^ n = 0
                                                                          theorem Nat.two_pow_pos (w : Nat) :
                                                                          0 < 2 ^ w
                                                                          instance Nat.instNeZeroHPow {n m : Nat} [NeZero n] :
                                                                          NeZero (n ^ m)
                                                                          theorem Nat.mul_pow (a b n : Nat) :
                                                                          (a * b) ^ n = a ^ n * b ^ n
                                                                          theorem Nat.pow_lt_pow_left {a b n : Nat} (hab : a < b) (h : n 0) :
                                                                          a ^ n < b ^ n
                                                                          theorem Nat.pow_left_inj {a b n : Nat} (hn : n 0) :
                                                                          a ^ n = b ^ n a = b

                                                                          min/max #

                                                                          @[reducible, inline]
                                                                          abbrev Nat.min (n m : Nat) :

                                                                          Returns the lesser of two natural numbers. Usually accessed via Min.min.

                                                                          Returns n if n ≤ m, or m if m ≤ n.

                                                                          Examples:

                                                                          Equations
                                                                            Instances For
                                                                              theorem Nat.min_def {n m : Nat} :
                                                                              min n m = if n m then n else m
                                                                              instance Nat.instMax :
                                                                              Equations
                                                                                @[reducible, inline]
                                                                                abbrev Nat.max (n m : Nat) :

                                                                                Returns the greater of two natural numbers. Usually accessed via Max.max.

                                                                                Returns m if n ≤ m, or n if m ≤ n.

                                                                                Examples:

                                                                                Equations
                                                                                  Instances For
                                                                                    theorem Nat.max_def {n m : Nat} :
                                                                                    max n m = if n m then m else n

                                                                                    Auxiliary theorems for well-founded recursion #

                                                                                    theorem Nat.ne_zero_of_lt {b a : Nat} (h : b < a) :
                                                                                    a 0
                                                                                    @[deprecated Nat.ne_zero_of_lt (since := "2025-02-06")]
                                                                                    theorem Nat.not_eq_zero_of_lt {b a : Nat} (h : b < a) :
                                                                                    a 0
                                                                                    theorem Nat.pred_lt_of_lt {n m : Nat} (h : m < n) :
                                                                                    n.pred < n
                                                                                    theorem Nat.sub_one_lt_of_lt {n m : Nat} (h : m < n) :
                                                                                    n - 1 < n

                                                                                    pred theorems #

                                                                                    theorem Nat.pred_succ (n : Nat) :
                                                                                    n.succ.pred = n
                                                                                    @[simp]
                                                                                    theorem Nat.zero_sub_one :
                                                                                    0 - 1 = 0
                                                                                    @[simp]
                                                                                    theorem Nat.add_one_sub_one (n : Nat) :
                                                                                    n + 1 - 1 = n
                                                                                    theorem Nat.sub_one_eq_self {n : Nat} :
                                                                                    n - 1 = n n = 0
                                                                                    theorem Nat.eq_self_sub_one {n : Nat} :
                                                                                    n = n - 1 n = 0
                                                                                    theorem Nat.succ_pred {a : Nat} (h : a 0) :
                                                                                    a.pred.succ = a
                                                                                    theorem Nat.sub_one_add_one {a : Nat} (h : a 0) :
                                                                                    a - 1 + 1 = a
                                                                                    theorem Nat.succ_pred_eq_of_pos {n : Nat} :
                                                                                    0 < nn.pred.succ = n
                                                                                    theorem Nat.sub_one_add_one_eq_of_pos {n : Nat} :
                                                                                    0 < nn - 1 + 1 = n
                                                                                    theorem Nat.eq_zero_or_eq_sub_one_add_one {n : Nat} :
                                                                                    n = 0 n = n - 1 + 1
                                                                                    @[simp]
                                                                                    theorem Nat.pred_eq_sub_one {n : Nat} :
                                                                                    n.pred = n - 1

                                                                                    sub theorems #

                                                                                    theorem Nat.add_sub_self_left (a b : Nat) :
                                                                                    a + b - a = b
                                                                                    theorem Nat.add_sub_self_right (a b : Nat) :
                                                                                    a + b - b = a
                                                                                    theorem Nat.sub_le_succ_sub (a i : Nat) :
                                                                                    a - i a.succ - i
                                                                                    theorem Nat.zero_lt_sub_of_lt {i a : Nat} (h : i < a) :
                                                                                    0 < a - i
                                                                                    theorem Nat.sub_succ_lt_self (a i : Nat) (h : i < a) :
                                                                                    a - (i + 1) < a - i
                                                                                    theorem Nat.sub_ne_zero_of_lt {a b : Nat} :
                                                                                    a < bb - a 0
                                                                                    theorem Nat.add_sub_of_le {a b : Nat} (h : a b) :
                                                                                    a + (b - a) = b
                                                                                    theorem Nat.sub_one_cancel {a b : Nat} :
                                                                                    0 < a0 < ba - 1 = b - 1a = b
                                                                                    @[simp]
                                                                                    theorem Nat.sub_add_cancel {n m : Nat} (h : m n) :
                                                                                    n - m + m = n
                                                                                    theorem Nat.add_sub_add_right (n k m : Nat) :
                                                                                    n + k - (m + k) = n - m
                                                                                    theorem Nat.add_sub_add_left (k n m : Nat) :
                                                                                    k + n - (k + m) = n - m
                                                                                    @[simp]
                                                                                    theorem Nat.add_sub_cancel (n m : Nat) :
                                                                                    n + m - m = n
                                                                                    @[simp]
                                                                                    theorem Nat.add_sub_cancel_left (n m : Nat) :
                                                                                    n + m - n = m
                                                                                    theorem Nat.add_sub_assoc {m k : Nat} (h : k m) (n : Nat) :
                                                                                    n + m - k = n + (m - k)
                                                                                    theorem Nat.eq_add_of_sub_eq {a b c : Nat} (hle : b a) (h : a - b = c) :
                                                                                    a = c + b
                                                                                    theorem Nat.sub_eq_of_eq_add {a b c : Nat} (h : a = c + b) :
                                                                                    a - b = c
                                                                                    theorem Nat.le_add_of_sub_le {a b c : Nat} (h : a - b c) :
                                                                                    a c + b
                                                                                    theorem Nat.sub_lt_sub_left {k m n : Nat} :
                                                                                    k < mk < nm - n < m - k
                                                                                    @[simp]
                                                                                    theorem Nat.zero_sub (n : Nat) :
                                                                                    0 - n = 0
                                                                                    theorem Nat.sub_lt_sub_right {a b c : Nat} :
                                                                                    c aa < ba - c < b - c
                                                                                    theorem Nat.sub_self_add (n m : Nat) :
                                                                                    n - (n + m) = 0
                                                                                    @[simp]
                                                                                    theorem Nat.sub_eq_zero_of_le {n m : Nat} (h : n m) :
                                                                                    n - m = 0
                                                                                    theorem Nat.sub_le_of_le_add {a b c : Nat} (h : a c + b) :
                                                                                    a - b c
                                                                                    theorem Nat.add_le_of_le_sub {a b c : Nat} (hle : b c) (h : a c - b) :
                                                                                    a + b c
                                                                                    theorem Nat.le_sub_of_add_le {a b c : Nat} (h : a + b c) :
                                                                                    a c - b
                                                                                    theorem Nat.add_lt_of_lt_sub {a b c : Nat} (h : a < c - b) :
                                                                                    a + b < c
                                                                                    theorem Nat.lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) :
                                                                                    a < c - b
                                                                                    theorem Nat.sub.elim {motive : NatProp} (x y : Nat) (h₁ : y x∀ (k : Nat), x = y + kmotive k) (h₂ : x < ymotive 0) :
                                                                                    motive (x - y)
                                                                                    theorem Nat.succ_sub {m n : Nat} (h : n m) :
                                                                                    m.succ - n = (m - n).succ
                                                                                    theorem Nat.sub_pos_of_lt {m n : Nat} (h : m < n) :
                                                                                    0 < n - m
                                                                                    theorem Nat.sub_sub (n m k : Nat) :
                                                                                    n - m - k = n - (m + k)
                                                                                    theorem Nat.sub_le_sub_left {n m : Nat} (h : n m) (k : Nat) :
                                                                                    k - m k - n
                                                                                    theorem Nat.sub_le_sub_right {n m : Nat} (h : n m) (k : Nat) :
                                                                                    n - k m - k
                                                                                    theorem Nat.sub_le_add_right_sub (a i j : Nat) :
                                                                                    a - i a + j - i
                                                                                    theorem Nat.lt_of_sub_ne_zero {n m : Nat} (h : n - m 0) :
                                                                                    m < n
                                                                                    theorem Nat.sub_ne_zero_iff_lt {n m : Nat} :
                                                                                    n - m 0 m < n
                                                                                    theorem Nat.lt_of_sub_pos {n m : Nat} (h : 0 < n - m) :
                                                                                    m < n
                                                                                    theorem Nat.lt_of_sub_eq_succ {m n l : Nat} (h : m - n = l.succ) :
                                                                                    n < m
                                                                                    theorem Nat.lt_of_sub_eq_sub_one {m n l : Nat} (h : m - n = l + 1) :
                                                                                    n < m
                                                                                    theorem Nat.sub_lt_left_of_lt_add {n k m : Nat} (H : n k) (h : k < n + m) :
                                                                                    k - n < m
                                                                                    theorem Nat.sub_lt_right_of_lt_add {n k m : Nat} (H : n k) (h : k < m + n) :
                                                                                    k - n < m
                                                                                    theorem Nat.le_of_sub_eq_zero {n m : Nat} :
                                                                                    n - m = 0n m
                                                                                    theorem Nat.le_of_sub_le_sub_right {n m k : Nat} :
                                                                                    k mn - k m - kn m
                                                                                    theorem Nat.sub_le_sub_iff_right {k m n : Nat} (h : k m) :
                                                                                    n - k m - k n m
                                                                                    theorem Nat.sub_eq_iff_eq_add {b a c : Nat} (h : b a) :
                                                                                    a - b = c a = c + b
                                                                                    theorem Nat.sub_eq_iff_eq_add' {b a c : Nat} (h : b a) :
                                                                                    a - b = c a = b + c
                                                                                    theorem Nat.sub_one_sub_lt_of_lt {a b : Nat} (h : a < b) :
                                                                                    b - 1 - a < b

                                                                                    Mul sub distrib #

                                                                                    theorem Nat.pred_mul (n m : Nat) :
                                                                                    n.pred * m = n * m - m
                                                                                    theorem Nat.sub_one_mul (n m : Nat) :
                                                                                    (n - 1) * m = n * m - m
                                                                                    theorem Nat.mul_pred (n m : Nat) :
                                                                                    n * m.pred = n * m - n
                                                                                    theorem Nat.mul_sub_one (n m : Nat) :
                                                                                    n * (m - 1) = n * m - n
                                                                                    theorem Nat.mul_sub_right_distrib (n m k : Nat) :
                                                                                    (n - m) * k = n * k - m * k
                                                                                    theorem Nat.sub_mul (n m k : Nat) :
                                                                                    (n - m) * k = n * k - m * k
                                                                                    theorem Nat.mul_sub_left_distrib (n m k : Nat) :
                                                                                    n * (m - k) = n * m - n * k
                                                                                    theorem Nat.mul_sub (n m k : Nat) :
                                                                                    n * (m - k) = n * m - n * k

                                                                                    Helper normalization theorems #

                                                                                    theorem Nat.not_le_eq (a b : Nat) :
                                                                                    (¬a b) = (b + 1 a)
                                                                                    theorem Nat.not_ge_eq (a b : Nat) :
                                                                                    (¬a b) = (a + 1 b)
                                                                                    theorem Nat.not_lt_eq (a b : Nat) :
                                                                                    (¬a < b) = (b a)
                                                                                    theorem Nat.not_gt_eq (a b : Nat) :
                                                                                    (¬a > b) = (a b)
                                                                                    theorem Nat.repeat_eq_repeatTR.go (α : Type u_1) (f : αα) (init : α) (m n : Nat) :
                                                                                    repeatTR.loop f m («repeat» f n init) = «repeat» f (m + n) init