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

Recursor identical to Nat.rec but uses notations 0 for Nat.zero and · + 1 for Nat.succ. Used as the default Nat eliminator by the induction tactic.

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

    Recursor identical to Nat.casesOn but uses notations 0 for Nat.zero and · + 1 for Nat.succ. Used as the default Nat eliminator by the cases tactic.

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

      Nat.fold evaluates f on the numbers up to n exclusive, in increasing order:

      • Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2
      Equations
      Instances For
        @[inline]
        def Nat.foldTR {α : Type u} (f : Natαα) (n : Nat) (init : α) :
        α

        Tail-recursive version of Nat.fold.

        Equations
        Instances For
          @[specialize #[]]
          def Nat.foldTR.loop {α : Type u} (f : Natαα) (n : Nat) :
          Natαα
          Equations
          Instances For
            @[specialize #[]]
            def Nat.foldRev {α : Type u} (f : Natαα) (n : Nat) (init : α) :
            α

            Nat.foldRev evaluates f on the numbers up to n exclusive, in decreasing order:

            Equations
            Instances For
              @[specialize #[]]
              def Nat.any (f : NatBool) :
              NatBool

              any f n = true iff there is i in [0, n-1] s.t. f i = true

              Equations
              Instances For
                @[inline]
                def Nat.anyTR (f : NatBool) (n : Nat) :

                Tail-recursive version of Nat.any.

                Equations
                Instances For
                  @[specialize #[]]
                  def Nat.anyTR.loop (f : NatBool) (n : Nat) :
                  NatBool
                  Equations
                  Instances For
                    @[specialize #[]]
                    def Nat.all (f : NatBool) :
                    NatBool

                    all f n = true iff every i in [0, n-1] satisfies f i = true

                    Equations
                    Instances For
                      @[inline]
                      def Nat.allTR (f : NatBool) (n : Nat) :

                      Tail-recursive version of Nat.all.

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

                          Nat.repeat f n a is f^(n) a; that is, it iterates f n times on a.

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

                            Tail-recursive version of Nat.repeat.

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

                                Boolean less-than of natural numbers.

                                Equations
                                • a.blt b = a.succ.ble b
                                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]
                                  @[simp]
                                  theorem Nat.add_eq {x : Nat} {y : Nat} :
                                  x.add y = x + y
                                  @[simp]
                                  theorem Nat.mul_eq {x : Nat} {y : Nat} :
                                  x.mul y = x * y
                                  @[simp]
                                  theorem Nat.sub_eq {x : Nat} {y : Nat} :
                                  x.sub y = x - y
                                  @[simp]
                                  theorem Nat.lt_eq {x : Nat} {y : Nat} :
                                  x.lt y = (x < y)
                                  @[simp]
                                  theorem Nat.le_eq {x : Nat} {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 : Nat} {y : Nat} :
                                  (x.beq y = true) = (x = y)
                                  @[simp]
                                  theorem Nat.ble_eq {x : Nat} {y : Nat} :
                                  (x.ble y = true) = (x y)
                                  @[simp]
                                  theorem Nat.blt_eq {x : Nat} {y : Nat} :
                                  (x.blt y = true) = (x < y)
                                  theorem Nat.beq_eq_true_eq (a : Nat) (b : Nat) :
                                  ((a == b) = true) = (a = b)
                                  theorem Nat.not_beq_eq_true_eq (a : Nat) (b : Nat) :
                                  ((!a == b) = true) = ¬a = b

                                  Nat.add theorems #

                                  @[simp]
                                  theorem Nat.zero_add (n : Nat) :
                                  0 + n = n
                                  theorem Nat.succ_add (n : Nat) (m : Nat) :
                                  n.succ + m = (n + m).succ
                                  theorem Nat.add_succ (n : Nat) (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
                                  @[simp]
                                  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 : Nat) (m : Nat) :
                                  n + m = m + n
                                  instance Nat.instCommutativeHAdd :
                                  Std.Commutative fun (x1 x2 : Nat) => x1 + x2
                                  Equations
                                  theorem Nat.add_assoc (n : Nat) (m : Nat) (k : Nat) :
                                  n + m + k = n + (m + k)
                                  instance Nat.instAssociativeHAdd :
                                  Std.Associative fun (x1 x2 : Nat) => x1 + x2
                                  Equations
                                  theorem Nat.add_left_comm (n : Nat) (m : Nat) (k : Nat) :
                                  n + (m + k) = m + (n + k)
                                  theorem Nat.add_right_comm (n : Nat) (m : Nat) (k : Nat) :
                                  n + m + k = n + k + m
                                  theorem Nat.add_left_cancel {n : Nat} {m : Nat} {k : Nat} :
                                  n + m = n + km = k
                                  theorem Nat.add_right_cancel {n : Nat} {m : Nat} {k : Nat} (h : n + m = k + m) :
                                  n = k
                                  theorem Nat.eq_zero_of_add_eq_zero {n : Nat} {m : Nat} :
                                  n + m = 0n = 0 m = 0
                                  theorem Nat.eq_zero_of_add_eq_zero_left {n : Nat} {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 : Nat) (m : Nat) :
                                  n * m.succ = n * m + n
                                  theorem Nat.mul_add_one (n : Nat) (m : Nat) :
                                  n * (m + 1) = n * m + n
                                  @[simp]
                                  theorem Nat.zero_mul (n : Nat) :
                                  0 * n = 0
                                  theorem Nat.succ_mul (n : Nat) (m : Nat) :
                                  n.succ * m = n * m + m
                                  theorem Nat.add_one_mul (n : Nat) (m : Nat) :
                                  (n + 1) * m = n * m + m
                                  theorem Nat.mul_comm (n : Nat) (m : Nat) :
                                  n * m = m * n
                                  instance Nat.instCommutativeHMul :
                                  Std.Commutative fun (x1 x2 : Nat) => x1 * x2
                                  Equations
                                  @[simp]
                                  theorem Nat.mul_one (n : Nat) :
                                  n * 1 = n
                                  @[simp]
                                  theorem Nat.one_mul (n : Nat) :
                                  1 * n = n
                                  theorem Nat.left_distrib (n : Nat) (m : Nat) (k : Nat) :
                                  n * (m + k) = n * m + n * k
                                  theorem Nat.right_distrib (n : Nat) (m : Nat) (k : Nat) :
                                  (n + m) * k = n * k + m * k
                                  theorem Nat.mul_add (n : Nat) (m : Nat) (k : Nat) :
                                  n * (m + k) = n * m + n * k
                                  theorem Nat.add_mul (n : Nat) (m : Nat) (k : Nat) :
                                  (n + m) * k = n * k + m * k
                                  theorem Nat.mul_assoc (n : Nat) (m : Nat) (k : Nat) :
                                  n * m * k = n * (m * k)
                                  instance Nat.instAssociativeHMul :
                                  Std.Associative fun (x1 x2 : Nat) => x1 * x2
                                  Equations
                                  theorem Nat.mul_left_comm (n : Nat) (m : Nat) (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 : Nat} {m : Nat} :
                                  n < mn.succ < m.succ
                                  theorem Nat.lt_succ_of_le {n : Nat} {m : Nat} :
                                  n mn < m.succ
                                  theorem Nat.le_of_lt_add_one {n : Nat} {m : Nat} :
                                  n < m + 1n m
                                  theorem Nat.lt_add_one_of_le {n : Nat} {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 : Nat) (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 : Nat) (m : Nat) :
                                  n - m n
                                  theorem Nat.sub_lt {n : Nat} {m : Nat} :
                                  0 < n0 < mn - m < n
                                  theorem Nat.sub_succ (n : Nat) (m : Nat) :
                                  n - m.succ = (n - m).pred
                                  theorem Nat.succ_sub_succ (n : Nat) (m : Nat) :
                                  n.succ - m.succ = n - m
                                  @[simp]
                                  theorem Nat.sub_self (n : Nat) :
                                  n - n = 0
                                  theorem Nat.sub_add_eq (a : Nat) (b : Nat) (c : Nat) :
                                  a - (b + c) = a - b - c
                                  theorem Nat.lt_of_lt_of_le {n : Nat} {m : Nat} {k : Nat} :
                                  n < mm kn < k
                                  theorem Nat.lt_of_lt_of_eq {n : Nat} {m : Nat} {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 : Nat} {m : Nat} (p : n = m) :
                                  n m
                                  theorem Nat.lt.step {n : Nat} {m : Nat} :
                                  n < mn < m.succ
                                  theorem Nat.le_of_succ_le {n : Nat} {m : Nat} (h : n.succ m) :
                                  n m
                                  theorem Nat.lt_of_succ_lt {n : Nat} {m : Nat} :
                                  n.succ < mn < m
                                  theorem Nat.le_of_lt {n : Nat} {m : Nat} :
                                  n < mn m
                                  theorem Nat.lt_of_succ_lt_succ {n : Nat} {m : Nat} :
                                  n.succ < m.succn < m
                                  theorem Nat.lt_of_succ_le {n : Nat} {m : Nat} (h : n.succ m) :
                                  n < m
                                  theorem Nat.succ_le_of_lt {n : Nat} {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.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 : Nat) (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 : Nat} {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 : Nat} {b : Nat} (h : a < b) :
                                  a b
                                  theorem Nat.le_or_eq_of_le_succ {m : Nat} {n : Nat} (h : m n.succ) :
                                  m n m = n.succ
                                  theorem Nat.le_or_eq_of_le_add_one {m : Nat} {n : Nat} (h : m n + 1) :
                                  m n m = n + 1
                                  @[simp]
                                  theorem Nat.le_add_right (n : Nat) (k : Nat) :
                                  n n + k
                                  @[simp]
                                  theorem Nat.le_add_left (n : Nat) (m : Nat) :
                                  n m + n
                                  theorem Nat.le_of_add_right_le {n : Nat} {m : Nat} {k : Nat} (h : n + k m) :
                                  n m
                                  theorem Nat.le_add_right_of_le {n : Nat} {m : Nat} {k : Nat} (h : n m) :
                                  n m + k
                                  theorem Nat.lt_of_add_one_le {n : Nat} {m : Nat} (h : n + 1 m) :
                                  n < m
                                  theorem Nat.add_one_le_of_lt {n : Nat} {m : Nat} (h : n < m) :
                                  n + 1 m
                                  theorem Nat.lt_add_left {a : Nat} {b : Nat} (c : Nat) (h : a < b) :
                                  a < c + b
                                  theorem Nat.lt_add_right {a : Nat} {b : Nat} (c : Nat) (h : a < b) :
                                  a < b + c
                                  theorem Nat.lt_of_add_right_lt {n : Nat} {m : Nat} {k : Nat} (h : n + k < m) :
                                  n < m
                                  theorem Nat.le.dest {n : Nat} {m : Nat} :
                                  n m∃ (k : Nat), n + k = m
                                  theorem Nat.le.intro {n : Nat} {m : Nat} {k : Nat} (h : n + k = m) :
                                  n m
                                  theorem Nat.not_le_of_gt {n : Nat} {m : Nat} (h : n > m) :
                                  ¬n m
                                  theorem Nat.not_le_of_lt {a : Nat} {b : Nat} :
                                  a < b¬b a
                                  theorem Nat.not_lt_of_ge {a : Nat} {b : Nat} :
                                  b a¬b < a
                                  theorem Nat.not_lt_of_le {a : Nat} {b : Nat} :
                                  a b¬b < a
                                  theorem Nat.lt_le_asymm {a : Nat} {b : Nat} :
                                  a < b¬b a
                                  theorem Nat.le_lt_asymm {a : Nat} {b : Nat} :
                                  a b¬b < a
                                  theorem Nat.gt_of_not_le {n : Nat} {m : Nat} (h : ¬n m) :
                                  n > m
                                  theorem Nat.lt_of_not_ge {a : Nat} {b : Nat} :
                                  ¬b ab < a
                                  theorem Nat.lt_of_not_le {a : Nat} {b : Nat} :
                                  ¬a bb < a
                                  theorem Nat.ge_of_not_lt {n : Nat} {m : Nat} (h : ¬n < m) :
                                  n m
                                  theorem Nat.le_of_not_gt {a : Nat} {b : Nat} :
                                  ¬b > ab a
                                  theorem Nat.le_of_not_lt {a : Nat} {b : Nat} :
                                  ¬a < bb a
                                  theorem Nat.ne_of_gt {a : Nat} {b : Nat} (h : b < a) :
                                  a b
                                  theorem Nat.ne_of_lt' {a : Nat} {b : Nat} :
                                  a < bb a
                                  @[simp]
                                  theorem Nat.not_le {a : Nat} {b : Nat} :
                                  ¬a b b < a
                                  @[simp]
                                  theorem Nat.not_lt {a : Nat} {b : Nat} :
                                  ¬a < b b a
                                  theorem Nat.le_of_not_le {a : Nat} {b : Nat} (h : ¬b a) :
                                  a b
                                  theorem Nat.le_of_not_ge {a : Nat} {b : Nat} :
                                  ¬a ba b
                                  theorem Nat.lt_trichotomy (a : Nat) (b : Nat) :
                                  a < b a = b b < a
                                  theorem Nat.lt_or_gt_of_ne {a : Nat} {b : Nat} (ne : a b) :
                                  a < b a > b
                                  theorem Nat.lt_or_lt_of_ne {a : Nat} {b : Nat} :
                                  a ba < b b < a
                                  theorem Nat.le_antisymm_iff {a : Nat} {b : Nat} :
                                  a = b a b b a
                                  theorem Nat.eq_iff_le_and_ge {a : Nat} {b : Nat} :
                                  a = b a b b a
                                  instance Nat.instAntisymmLe :
                                  Antisymm fun (x1 x2 : Nat) => x1 x2
                                  Equations
                                  instance Nat.instAntisymmNotLt :
                                  Antisymm fun (x1 x2 : Nat) => ¬x1 < x2
                                  Equations
                                  theorem Nat.add_le_add_left {n : Nat} {m : Nat} (h : n m) (k : Nat) :
                                  k + n k + m
                                  theorem Nat.add_le_add_right {n : Nat} {m : Nat} (h : n m) (k : Nat) :
                                  n + k m + k
                                  theorem Nat.add_lt_add_left {n : Nat} {m : Nat} (h : n < m) (k : Nat) :
                                  k + n < k + m
                                  theorem Nat.add_lt_add_right {n : Nat} {m : Nat} (h : n < m) (k : Nat) :
                                  n + k < m + k
                                  theorem Nat.lt_add_of_pos_right {k : Nat} {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 : Nat} {b : Nat} {c : Nat} {d : Nat} (h₁ : a b) (h₂ : c d) :
                                  a + c b + d
                                  theorem Nat.add_lt_add {a : Nat} {b : Nat} {c : Nat} {d : Nat} (h₁ : a < b) (h₂ : c < d) :
                                  a + c < b + d
                                  theorem Nat.le_of_add_le_add_left {a : Nat} {b : Nat} {c : Nat} (h : a + b a + c) :
                                  b c
                                  theorem Nat.le_of_add_le_add_right {a : Nat} {b : Nat} {c : Nat} :
                                  a + b c + ba c
                                  @[simp]
                                  theorem Nat.add_le_add_iff_right {m : Nat} {k : Nat} {n : Nat} :
                                  m + n k + n m k

                                  le/lt #

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

                                  Alias for Nat.lt_asymm.

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

                                    Alias for Nat.lt_asymm.

                                    Equations
                                    Instances For
                                      theorem Nat.lt_iff_le_not_le {m : Nat} {n : Nat} :
                                      m < n m n ¬n m
                                      @[reducible, inline]
                                      abbrev Nat.lt_iff_le_and_not_ge {m : Nat} {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 : Nat} {n : Nat} :
                                        m < n m n m n
                                        theorem Nat.ne_iff_lt_or_gt {a : Nat} {b : Nat} :
                                        a b a < b b < a
                                        @[reducible, inline]
                                        abbrev Nat.lt_or_gt {a : Nat} {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 : Nat) (n : Nat) :
                                          m n n m

                                          Alias for Nat.le_total.

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

                                            Alias for Nat.le_total.

                                            Equations
                                            Instances For
                                              theorem Nat.eq_or_lt_of_not_lt {a : Nat} {b : Nat} (hnlt : ¬a < b) :
                                              a = b b < a
                                              theorem Nat.lt_or_eq_of_le {n : Nat} {m : Nat} (h : n m) :
                                              n < m n = m
                                              theorem Nat.le_iff_lt_or_eq {n : Nat} {m : Nat} :
                                              n m n < m n = m
                                              theorem Nat.lt_succ_iff {m : Nat} {n : Nat} :
                                              m < n.succ m n
                                              theorem Nat.lt_add_one_iff {m : Nat} {n : Nat} :
                                              m < n + 1 m n
                                              theorem Nat.lt_succ_iff_lt_or_eq {m : Nat} {n : Nat} :
                                              m < n.succ m < n m = n
                                              theorem Nat.lt_add_one_iff_lt_or_eq {m : Nat} {n : Nat} :
                                              m < n + 1 m < n m = n
                                              theorem Nat.eq_of_lt_succ_of_not_lt {m : Nat} {n : Nat} (hmn : m < n + 1) (h : ¬m < n) :
                                              m = n
                                              theorem Nat.eq_of_le_of_lt_succ {n : Nat} {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 #

                                                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 : Nat} {m : Nat} :
                                                n.succ m n < m
                                                theorem Nat.add_one_le_iff {n : Nat} {m : Nat} :
                                                n + 1 m n < m
                                                theorem Nat.lt_succ {m : Nat} {n : Nat} :
                                                m < n.succ m n
                                                theorem Nat.lt_succ_of_lt {a : Nat} {b : Nat} (h : a < b) :
                                                a < b.succ
                                                theorem Nat.lt_add_one_of_lt {a : Nat} {b : Nat} (h : a < b) :
                                                a < b + 1
                                                theorem Nat.succ_pred_eq_of_ne_zero {n : Nat} :
                                                n 0n.pred.succ = n
                                                theorem Nat.eq_zero_or_eq_succ_pred (n : Nat) :
                                                n = 0 n = n.pred.succ
                                                theorem Nat.succ_inj' {a : Nat} {b : Nat} :
                                                a.succ = b.succ a = b
                                                theorem Nat.succ_le_succ_iff {a : Nat} {b : Nat} :
                                                a.succ b.succ a b
                                                theorem Nat.succ_lt_succ_iff {a : Nat} {b : Nat} :
                                                a.succ < b.succ a < b
                                                theorem Nat.add_one_inj {a : Nat} {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 : Nat} {b : Nat} :
                                                a + 1 b + 1 a b
                                                theorem Nat.add_one_lt_add_one_iff {a : Nat} {b : Nat} :
                                                a + 1 < b + 1 a < b
                                                theorem Nat.pred_inj {a : Nat} {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 : Nat} {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 : Nat} {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 : Nat} {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 : Nat} {m : Nat} (h : n < m) :
                                                n m.pred
                                                theorem Nat.le_sub_one_of_lt {a : Nat} {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 : Nat} {n : Nat} (h : 0 < m) :
                                                n m - 1n < m
                                                theorem Nat.le_sub_one_iff_lt {m : Nat} {n : Nat} (h : 0 < m) :
                                                n m - 1 n < m
                                                theorem Nat.exists_eq_succ_of_ne_zero {n : Nat} :
                                                n 0∃ (k : Nat), n = k.succ
                                                theorem Nat.exists_eq_add_one_of_ne_zero {n : Nat} :
                                                n 0∃ (k : Nat), n = k + 1

                                                Basic theorems for comparing numerals #

                                                theorem Nat.succ_ne_zero (n : Nat) :
                                                n.succ 0

                                                mul + order #

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

                                                power #

                                                theorem Nat.pow_succ (n : Nat) (m : Nat) :
                                                n ^ m.succ = n ^ m * n
                                                theorem Nat.pow_add_one (n : Nat) (m : Nat) :
                                                n ^ (m + 1) = n ^ m * n
                                                @[simp]
                                                theorem Nat.pow_zero (n : Nat) :
                                                n ^ 0 = 1
                                                theorem Nat.pow_le_pow_of_le_left {n : Nat} {m : Nat} (h : n m) (i : Nat) :
                                                n ^ i m ^ i
                                                theorem Nat.pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} {j : Nat} :
                                                i jn ^ i n ^ j
                                                theorem Nat.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) :
                                                0 < n ^ m
                                                @[simp]
                                                theorem Nat.zero_pow_of_pos (n : Nat) (h : 0 < n) :
                                                0 ^ n = 0

                                                min/max #

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

                                                Nat.min a b is the minimum of a and b:

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

                                                  Nat.max a b is the maximum of a and b:

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

                                                    Auxiliary theorems for well-founded recursion #

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

                                                      Mul sub distrib #

                                                      theorem Nat.pred_mul (n : Nat) (m : Nat) :
                                                      n.pred * m = n * m - m
                                                      @[reducible, inline, deprecated]
                                                      abbrev Nat.mul_pred_left (n : Nat) (m : Nat) :
                                                      n.pred * m = n * m - m
                                                      Equations
                                                      Instances For
                                                        theorem Nat.sub_one_mul (n : Nat) (m : Nat) :
                                                        (n - 1) * m = n * m - m
                                                        theorem Nat.mul_pred (n : Nat) (m : Nat) :
                                                        n * m.pred = n * m - n
                                                        @[reducible, inline, deprecated]
                                                        abbrev Nat.mul_pred_right (n : Nat) (m : Nat) :
                                                        n * m.pred = n * m - n
                                                        Equations
                                                        Instances For
                                                          theorem Nat.mul_sub_one (n : Nat) (m : Nat) :
                                                          n * (m - 1) = n * m - n
                                                          theorem Nat.mul_sub_right_distrib (n : Nat) (m : Nat) (k : Nat) :
                                                          (n - m) * k = n * k - m * k
                                                          theorem Nat.mul_sub_left_distrib (n : Nat) (m : Nat) (k : Nat) :
                                                          n * (m - k) = n * m - n * k

                                                          Helper normalization theorems #

                                                          theorem Nat.not_le_eq (a : Nat) (b : Nat) :
                                                          (¬a b) = (b + 1 a)
                                                          theorem Nat.not_ge_eq (a : Nat) (b : Nat) :
                                                          (¬a b) = (a + 1 b)
                                                          theorem Nat.not_lt_eq (a : Nat) (b : Nat) :
                                                          (¬a < b) = (b a)
                                                          theorem Nat.not_gt_eq (a : Nat) (b : Nat) :
                                                          (¬a > b) = (a b)

                                                          csimp theorems #

                                                          theorem Nat.fold_eq_foldTR.go (α : Type u_1) (f : Natαα) (init : α) (m : Nat) (n : Nat) :
                                                          Nat.foldTR.loop f (m + n) m (Nat.fold f n init) = Nat.fold f (m + n) init
                                                          theorem Nat.any_eq_anyTR.go (f : NatBool) (m : Nat) (n : Nat) :
                                                          (Nat.any f n || Nat.anyTR.loop f (m + n) m) = Nat.any f (m + n)
                                                          theorem Nat.all_eq_allTR.go (f : NatBool) (m : Nat) (n : Nat) :
                                                          (Nat.all f n && Nat.allTR.loop f (m + n) m) = Nat.all f (m + n)
                                                          theorem Nat.repeat_eq_repeatTR.go (α : Type u_1) (f : αα) (init : α) (m : Nat) (n : Nat) :
                                                          Nat.repeatTR.loop f m (Nat.repeat f n init) = Nat.repeat f (m + n) init
                                                          @[inline]
                                                          def Prod.foldI {α : Type u} (f : Natαα) (i : Nat × Nat) (a : α) :
                                                          α

                                                          (start, stop).foldI f a evaluates f on all the numbers from start (inclusive) to stop (exclusive) in increasing order:

                                                          • (5, 8).foldI f init = init |> f 5 |> f 6 |> f 7
                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def Prod.anyI (f : NatBool) (i : Nat × Nat) :

                                                            (start, stop).anyI f a returns true if f is true for some natural number from start (inclusive) to stop (exclusive):

                                                            • (5, 8).anyI f = f 5 || f 6 || f 7
                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              def Prod.allI (f : NatBool) (i : Nat × Nat) :

                                                              (start, stop).allI f a returns true if f is true for all natural numbers from start (inclusive) to stop (exclusive):

                                                              • (5, 8).anyI f = f 5 && f 6 && f 7
                                                              Equations
                                                              Instances For