Documentation

Arithmetization.Basic.IOpen

theorem LO.Arith.open_induction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {P : VProp} (hP : ∃ (p : LO.FirstOrder.Semiformula ℒₒᵣ V 1), p.Open ∀ (x : V), P x (LO.FirstOrder.Semiformula.Evalm V ![x] id) p) (zero : P 0) (succ : ∀ (x : V), P xP (x + 1)) (x : V) :
P x
theorem LO.Arith.open_leastNumber {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {P : VProp} (hP : ∃ (p : LO.FirstOrder.Semiformula ℒₒᵣ V 1), p.Open ∀ (x : V), P x (LO.FirstOrder.Semiformula.Evalm V ![x] id) p) (zero : P 0) {a : V} (counterex : ¬P a) :
∃ (x : V), P x ¬P (x + 1)
theorem LO.Arith.div_exists_unique_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) :
∃! u : V, b * u a a < b * (u + 1)
theorem LO.Arith.div_exists_unique {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
∃! u : V, (0 < bb * u a a < b * (u + 1)) (b = 0u = 0)
Equations
Instances For
    theorem LO.Arith.mul_div_le_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (h : 0 < b) :
    b * (a / b) a
    theorem LO.Arith.lt_mul_div_succ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (h : 0 < b) :
    a < b * (a / b + 1)
    theorem LO.Arith.eq_mul_div_add_of_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (hb : 0 < b) :
    r < b, a = b * (a / b) + r
    @[simp]
    theorem LO.Arith.div_spec_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
    a / 0 = 0
    theorem LO.Arith.div_graph {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} {c : V} :
    c = a / b (0 < bb * c a a < b * (c + 1)) (b = 0c = 0)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem LO.Arith.div_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
      theorem LO.Arith.div_spec_of_pos' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (h : 0 < b) :
      v < b, a = a / b * b + v
      theorem LO.Arith.div_eq_of {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {c : V} {a : V} {b : V} (hb : b * c a) (ha : a < b * (c + 1)) :
      a / b = c
      theorem LO.Arith.div_mul_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) {r : V} (hr : r < b) :
      (a * b + r) / b = a
      theorem LO.Arith.div_mul_add' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) {r : V} (hr : r < b) :
      (b * a + r) / b = a
      @[simp]
      theorem LO.Arith.zero_div {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
      0 / a = 0
      theorem LO.Arith.div_mul {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) (c : V) :
      a / (b * c) = a / b / c
      @[simp]
      theorem LO.Arith.mul_div_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
      b * (a / b) a
      @[simp]
      theorem LO.Arith.div_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
      a / b a
      instance LO.Arith.div_polybounded {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
      LO.FirstOrder.Arith.Bounded₂ fun (x x_1 : V) => x / x_1
      Equations
      • =
      instance LO.Arith.div_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
      𝚺₀-Function₂ fun (x x_1 : V) => x / x_1
      Equations
      • =
      @[simp]
      theorem LO.Arith.div_mul_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
      a / b * b a
      theorem LO.Arith.lt_mul_div {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) :
      a < b * (a / b + 1)
      @[simp]
      theorem LO.Arith.div_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
      a / 1 = a
      theorem LO.Arith.div_add_mul_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (c : V) {b : V} (pos : 0 < b) :
      (a + c * b) / b = a / b + c
      theorem LO.Arith.div_add_mul_self' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (c : V) {b : V} (pos : 0 < b) :
      (a + b * c) / b = a / b + c
      theorem LO.Arith.div_mul_add_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (c : V) {b : V} (pos : 0 < b) :
      (a * b + c) / b = a + c / b
      theorem LO.Arith.div_mul_add_self' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (c : V) {b : V} (pos : 0 < b) :
      (b * a + c) / b = a + c / b
      @[simp]
      theorem LO.Arith.div_mul_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) :
      a * b / b = a
      @[simp]
      theorem LO.Arith.div_mul_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) :
      b * a / b = a
      @[simp]
      theorem LO.Arith.div_eq_zero_of_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (b : V) {a : V} (h : a < b) :
      a / b = 0
      @[simp]
      theorem LO.Arith.div_sq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
      a ^ 2 / a = a
      @[simp]
      theorem LO.Arith.div_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} (hx : 0 < a) :
      a / a = 1
      @[simp]
      theorem LO.Arith.div_mul' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) :
      b * a / b = a
      @[simp]
      theorem LO.Arith.div_add_self_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} (pos : 0 < a) (b : V) :
      (a + b) / a = 1 + b / a
      @[simp]
      theorem LO.Arith.div_add_self_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) :
      (a + b) / b = a / b + 1
      theorem LO.Arith.mul_div_self_of_dvd {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} :
      a * (b / a) = b a b
      theorem LO.Arith.div_lt_of_pos_of_one_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} (ha : 0 < a) (hb : 1 < b) :
      a / b < a
      theorem LO.Arith.le_two_mul_div_two_add_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
      a 2 * (a / 2) + 1
      theorem LO.Arith.div_monotone {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} (h : a b) (c : V) :
      a / c b / c
      theorem LO.Arith.div_lt_of_lt_mul {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} {c : V} (h : a < b * c) :
      a / c < b
      theorem LO.Arith.div_cancel_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {c : V} (pos : 0 < c) (a : V) (b : V) :
      c * a / (c * b) = a / b
      theorem LO.Arith.div_cancel_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {c : V} (pos : 0 < c) (a : V) (b : V) :
      a * c / (b * c) = a / b
      @[simp]
      theorem LO.Arith.two_mul_add_one_div_two {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
      (2 * a + 1) / 2 = a
      def LO.Arith.rem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
      V
      Equations
      Instances For
        Equations
        • LO.Arith.instMod_arithmetization = { mod := LO.Arith.rem }
        Instances For
          theorem LO.Arith.mod_def {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
          a % b = a - b * (a / b)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem LO.Arith.rem_graph {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) (c : V) :
            a = b % c xb, x = b / c a = b - c * x
            theorem LO.Arith.rem_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
            instance LO.Arith.rem_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
            𝚺₀-Function₂ fun (x x_1 : V) => x % x_1
            Equations
            • =
            theorem LO.Arith.div_add_mod {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
            b * (a / b) + a % b = a
            @[simp]
            theorem LO.Arith.mod_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            a % 0 = a
            @[simp]
            theorem LO.Arith.zero_mod {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            0 % a = 0
            @[simp]
            theorem LO.Arith.mod_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            a % a = 0
            theorem LO.Arith.mod_mul_add_of_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) {r : V} (hr : r < b) :
            (a * b + r) % b = r
            @[simp]
            theorem LO.Arith.mod_mul_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (c : V) (pos : 0 < b) :
            (a * b + c) % b = c % b
            @[simp]
            theorem LO.Arith.mod_add_mul {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {c : V} (a : V) (b : V) (pos : 0 < c) :
            (a + b * c) % c = a % c
            @[simp]
            theorem LO.Arith.mod_add_mul' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {c : V} (a : V) (b : V) (pos : 0 < c) :
            (a + c * b) % c = a % c
            @[simp]
            theorem LO.Arith.mod_mul_add' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (c : V) (pos : 0 < b) :
            (b * a + c) % b = c % b
            @[simp]
            theorem LO.Arith.mod_mul_self_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
            a * b % b = 0
            @[simp]
            theorem LO.Arith.mod_mul_self_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
            b * a % b = 0
            @[simp]
            theorem LO.Arith.mod_eq_self_of_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} (h : a < b) :
            a % b = a
            @[simp]
            theorem LO.Arith.mod_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) :
            a % b < b
            @[simp]
            theorem LO.Arith.mod_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
            a % b a
            instance LO.Arith.mod_polybounded {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
            LO.FirstOrder.Arith.Bounded₂ fun (x x_1 : V) => x % x_1
            Equations
            • =
            theorem LO.Arith.mod_eq_zero_iff_dvd {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} :
            b % a = 0 a b
            @[simp]
            theorem LO.Arith.mod_add_remove_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} (pos : 0 < b) :
            (a + b) % b = a % b
            theorem LO.Arith.mod_add_remove_right_of_dvd {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} {m : V} (h : m b) (pos : 0 < m) :
            (a + b) % m = a % m
            @[simp]
            theorem LO.Arith.mod_add_remove_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} (pos : 0 < a) :
            (a + b) % a = b % a
            theorem LO.Arith.mod_add_remove_left_of_dvd {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} {m : V} (h : m a) (pos : 0 < m) :
            (a + b) % m = b % m
            theorem LO.Arith.mod_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} {m : V} (pos : 0 < m) :
            (a + b) % m = (a % m + b % m) % m
            theorem LO.Arith.mod_mul {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} {m : V} (pos : 0 < m) :
            a * b % m = a % m * (b % m) % m
            @[simp]
            theorem LO.Arith.mod_div {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
            a % b / b = 0
            @[simp]
            theorem LO.Arith.mod_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            a % 1 = 0
            theorem LO.Arith.mod_two {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            a % 2 = 0 a % 2 = 1
            @[simp]
            theorem LO.Arith.mod_two_not_zero_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} :
            ¬a % 2 = 0 a % 2 = 1
            @[simp]
            theorem LO.Arith.mod_two_not_one_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} :
            ¬a % 2 = 1 a % 2 = 0
            theorem LO.Arith.two_dvd_mul {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} :
            2 a * b2 a 2 b
            theorem LO.Arith.even_or_odd {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            ∃ (x : V), a = 2 * x a = 2 * x + 1
            theorem LO.Arith.even_or_odd' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            a = 2 * (a / 2) a = 2 * (a / 2) + 1
            theorem LO.Arith.two_prime {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
            theorem LO.Arith.sqrt_exists_unique {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            ∃! x : V, x * x a a < (x + 1) * (x + 1)
            def LO.Arith.sqrt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
            V
            Equations
            Instances For
              @[simp]
              theorem LO.Arith.sqrt_spec_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
              a * a a
              @[simp]
              theorem LO.Arith.sqrt_spec_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
              a < (a + 1) * (a + 1)
              theorem LO.Arith.sqrt_graph {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} :
              b = a b * b a a < (b + 1) * (b + 1)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                instance LO.Arith.sqrt_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                𝚺₀-Function₁ fun (x : V) => x
                Equations
                • =
                theorem LO.Arith.eq_sqrt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (x : V) (a : V) :
                x * x a a < (x + 1) * (x + 1)x = a
                theorem LO.Arith.sqrt_eq_of_le_of_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {x : V} {a : V} (le : x * x a) (lt : a < (x + 1) * (x + 1)) :
                a = x
                theorem LO.Arith.sqrt_eq_of_le_of_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {x : V} {a : V} (le : x * x a) (h : a x * x + 2 * x) :
                a = x
                @[simp]
                theorem LO.Arith.sq_sqrt_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                (a) ^ 2 a
                @[simp]
                theorem LO.Arith.sqrt_lt_sq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                a < (a + 1) ^ 2
                @[simp]
                theorem LO.Arith.sqrt_mul_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                (a * a) = a
                @[simp]
                theorem LO.Arith.sqrt_sq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                a ^ 2 = a
                @[simp]
                theorem LO.Arith.sqrt_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                0 = 0
                @[simp]
                theorem LO.Arith.sqrt_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                1 = 1
                theorem LO.Arith.sqrt_two {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                2 = 1
                theorem LO.Arith.sqrt_three {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                3 = 1
                @[simp]
                theorem LO.Arith.sqrt_four {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                4 = 2
                @[simp]
                theorem LO.Arith.two_ne_square {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                2 a ^ 2
                @[simp]
                theorem LO.Arith.sqrt_le_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                a a * a + 2 * a
                @[simp]
                theorem LO.Arith.sqrt_le_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                a a
                instance LO.Arith.instBounded₁Sqrt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                Equations
                • =
                theorem LO.Arith.sqrt_lt_self_of_one_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} (h : 1 < a) :
                a < a
                theorem LO.Arith.sqrt_le_of_le_sq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} :
                a b ^ 2a b
                theorem LO.Arith.sq_lt_of_lt_sqrt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a : V} {b : V} :
                a < ba ^ 2 < b
                def LO.Arith.pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) (b : V) :
                V
                Equations
                • a, b = if a < b then b * b + a else a * a + a + b
                Instances For

                  !⟪x, y, z, ...⟫ notation for Seq

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem LO.Arith.pair_graph {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} {b : V} {c : V} :
                      c = a, b a < b c = b * b + a b a c = a * a + a + b
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem LO.Arith.pair_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] :
                        instance LO.Arith.pair_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] :
                        𝚺₀-Function₂ LO.Arith.pair
                        Equations
                        • =
                        instance LO.Arith.instBounded₂Pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] :
                        Equations
                        • =
                        def LO.Arith.unpair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                        V × V
                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev LO.Arith.pi₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                          V
                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev LO.Arith.pi₂ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                            V
                            Equations
                            Instances For
                              @[simp]
                              theorem LO.Arith.pair_unpair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                              π₁ a, π₂ a = a
                              @[simp]
                              theorem LO.Arith.unpair_pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
                              LO.Arith.unpair a, b = (a, b)
                              @[simp]
                              theorem LO.Arith.pi₁_pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
                              π₁a, b = a
                              @[simp]
                              theorem LO.Arith.pi₂_pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
                              π₂a, b = b
                              def LO.Arith.pairEquiv {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                              V × V V
                              Equations
                              • LO.Arith.pairEquiv = { toFun := Function.uncurry LO.Arith.pair, invFun := LO.Arith.unpair, left_inv := , right_inv := }
                              Instances For
                                @[simp]
                                theorem LO.Arith.pi₁_le_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                                @[simp]
                                theorem LO.Arith.pi₂_le_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) :
                                @[simp]
                                theorem LO.Arith.le_pair_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
                                a a, b
                                @[simp]
                                theorem LO.Arith.le_pair_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (a : V) (b : V) :
                                b a, b
                                @[simp]
                                theorem LO.Arith.lt_pair_left_of_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} (pos : 0 < a) (b : V) :
                                a < a, b
                                instance LO.Arith.instBounded₁Pi₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                Equations
                                • =
                                instance LO.Arith.instBounded₁Pi₂ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                Equations
                                • =
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    instance LO.Arith.pi₁_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                    𝚺₀-Function₁ LO.Arith.pi₁
                                    Equations
                                    • =
                                    instance LO.Arith.pi₂_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                    𝚺₀-Function₁ LO.Arith.pi₂
                                    Equations
                                    • =
                                    theorem LO.Arith.pair_lt_pair_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {a₁ : V} {a₂ : V} (h : a₁ < a₂) (b : V) :
                                    a₁, b < a₂, b
                                    theorem LO.Arith.pair_le_pair_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {a₁ : V} {a₂ : V} (h : a₁ a₂) (b : V) :
                                    a₁, b a₂, b
                                    theorem LO.Arith.pair_lt_pair_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) {b₁ : V} {b₂ : V} (h : b₁ < b₂) :
                                    a, b₁ < a, b₂
                                    theorem LO.Arith.pair_le_pair_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) {b₁ : V} {b₂ : V} (h : b₁ b₂) :
                                    a, b₁ a, b₂
                                    theorem LO.Arith.pair_le_pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {a₁ : V} {a₂ : V} {b₁ : V} {b₂ : V} (ha : a₁ a₂) (hb : b₁ b₂) :
                                    a₁, b₁ a₂, b₂
                                    theorem LO.Arith.pair_lt_pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {a₁ : V} {a₂ : V} {b₁ : V} {b₂ : V} (ha : a₁ < a₂) (hb : b₁ < b₂) :
                                    a₁, b₁ < a₂, b₂
                                    @[simp]
                                    theorem LO.Arith.pair_polybound {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) (b : V) :
                                    a, b (a + b + 1) ^ 2
                                    @[simp]
                                    theorem LO.Arith.pair_ext_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {a₁ : V} {a₂ : V} {b₁ : V} {b₂ : V} :
                                    a₁, b₁ = a₂, b₂ a₁ = a₂ b₁ = b₂
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem LO.Arith.pair₃_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                            𝚺₀-Function₃ fun (x x_1 x_2 : V) => x, x_1, x_2 via LO.FirstOrder.Arith.pair₃Def
                                            @[simp]
                                            theorem LO.Arith.eval_pair₃Def {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (v : Fin 4V) :
                                            theorem LO.Arith.pair₄_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                            𝚺₀-Function₄ fun (x x_1 x_2 x_3 : V) => x, x_1, x_2, x_3 via LO.FirstOrder.Arith.pair₄Def
                                            @[simp]
                                            theorem LO.Arith.eval_pair₄Def {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (v : Fin 5V) :
                                            theorem LO.Arith.pair₅_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                            LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 5V) => v 0, v 1, v 2, v 3, v 4) LO.FirstOrder.Arith.pair₅Def
                                            @[simp]
                                            theorem LO.Arith.eval_pair₅Def {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (v : Fin 6V) :
                                            V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.pair₅Def) v 0 = v 1, v 2, v 3, v 4, v 5
                                            theorem LO.Arith.pair₆_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] :
                                            LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 6V) => v 0, v 1, v 2, v 3, v 4, v 5) LO.FirstOrder.Arith.pair₆Def
                                            @[simp]
                                            theorem LO.Arith.eval_pair₆Def {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (v : Fin 7V) :
                                            V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.pair₆Def) v 0 = v 1, v 2, v 3, v 4, v 5, v 6
                                            def LO.Arith.npair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {n : } (v : Fin nV) :
                                            V
                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem LO.Arith.npair_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] (v : Fin 0V) :
                                              theorem LO.Arith.npair_succ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] {n : } (x : V) (v : Fin nV) :
                                              def LO.Arith.unNpair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {n : } :
                                              Fin nVV
                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem LO.Arith.unNpair_npair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] {n : } (i : Fin n) (v : Fin nV) :
                                                def LO.FirstOrder.Arith.unNpairDef {n : } (i : Fin n) :
                                                𝚺₀.Semisentence 2
                                                Equations
                                                Instances For
                                                  @[simp]
                                                  Equations
                                                  • =
                                                  theorem LO.Arith.hierarchy_polynomial_induction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈open] (Γ : LO.Polarity) (m : ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)] {P : VProp} (hP : { Γ := Γ.coe, rank := m }-Predicate P) (zero : P 0) (even : x > 0, P xP (2 * x)) (odd : ∀ (x : V), P xP (2 * x + 1)) (x : V) :
                                                  P x
                                                  theorem LO.Arith.hierarchy_polynomial_induction_oRing_sigma₀ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈𝚺₀] {P : VProp} (hP : 𝚺₀-Predicate P) (zero : P 0) (even : x > 0, P xP (2 * x)) (odd : ∀ (x : V), P xP (2 * x + 1)) (x : V) :
                                                  P x
                                                  theorem LO.Arith.hierarchy_polynomial_induction_oRing_sigma₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚺₁-Predicate P) (zero : P 0) (even : x > 0, P xP (2 * x)) (odd : ∀ (x : V), P xP (2 * x + 1)) (x : V) :
                                                  P x
                                                  theorem LO.Arith.hierarchy_polynomial_induction_oRing_pi₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] [V ⊧ₘ* 𝐈𝚷₁] {P : VProp} (hP : 𝚷₁-Predicate P) (zero : P 0) (even : x > 0, P xP (2 * x)) (odd : ∀ (x : V), P xP (2 * x + 1)) (x : V) :
                                                  P x
                                                  theorem LO.Arith.nat_cast_pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] (n : ) (m : ) :
                                                  n, m = n, m
                                                  theorem LO.Arith.nat_pair_eq (m : ) (n : ) :
                                                  n, m = Nat.pair n m
                                                  theorem LO.Arith.pair_coe_eq_coe_pair {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻] (m : ) (n : ) :
                                                  n, m = (Nat.pair n m)