theorem
LO.Arith.log_exists_unique_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
(hy : 0 < y)
:
Equations
Instances For
@[simp]
theorem
LO.Arith.log_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
(pos : 0 < y)
:
∃ y' ≤ y, LO.Arith.Exponential (LO.Arith.log y) y' ∧ y < 2 * y'
theorem
LO.Arith.log_lt_self_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
(pos : 0 < y)
:
LO.Arith.log y < y
@[simp]
theorem
LO.Arith.log_le_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
:
LO.Arith.log a ≤ a
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.log_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₁ LO.Arith.log via LO.FirstOrder.Arith.logDef
@[simp]
instance
LO.Arith.log_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₁ LO.Arith.log
Equations
- ⋯ = ⋯
instance
LO.Arith.instBounded₁Log
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
LO.FirstOrder.Arith.Bounded₁ LO.Arith.log
Equations
- ⋯ = ⋯
theorem
LO.Arith.log_eq_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(pos : 0 < y)
{y' : V}
(H : LO.Arith.Exponential x y')
(hy' : y' ≤ y)
(hy : y < 2 * y')
:
LO.Arith.log y = x
@[simp]
@[simp]
theorem
LO.Arith.log_two_mul_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
(pos : 0 < y)
:
LO.Arith.log (2 * y) = LO.Arith.log y + 1
theorem
LO.Arith.log_two_mul_add_one_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
(pos : 0 < y)
:
LO.Arith.log (2 * y + 1) = LO.Arith.log y + 1
theorem
LO.Arith.Exponential.log_eq_of_exp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(H : LO.Arith.Exponential x y)
:
LO.Arith.log y = x
theorem
LO.Arith.exponential_of_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{p : V}
(pp : LO.Arith.Pow2 p)
:
theorem
LO.Arith.log_mul_pow2_add_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{p : V}
{b : V}
(pos : 0 < a)
(pp : LO.Arith.Pow2 p)
(hb : b < p)
:
LO.Arith.log (a * p + b) = LO.Arith.log a + LO.Arith.log p
theorem
LO.Arith.log_mul_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{p : V}
(pos : 0 < a)
(pp : LO.Arith.Pow2 p)
:
LO.Arith.log (a * p) = LO.Arith.log a + LO.Arith.log p
theorem
LO.Arith.log_monotone
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{b : V}
(h : a ≤ b)
:
Equations
- LO.Arith.binaryLength a = if 0 < a then LO.Arith.log a + 1 else 0
Instances For
Equations
- LO.Arith.instLength = { length := LO.Arith.binaryLength }
Instances For
theorem
LO.Arith.length_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
(pos : 0 < a)
:
‖a‖ = LO.Arith.log a + 1
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.length_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₁ fun (x : V) => ‖x‖ via LO.FirstOrder.Arith.lengthDef
@[simp]
instance
LO.Arith.length_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₁ fun (x : V) => ‖x‖
Equations
- ⋯ = ⋯
instance
LO.Arith.instBounded₁Length
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
LO.FirstOrder.Arith.Bounded₁ fun (x : V) => ‖x‖
Equations
- ⋯ = ⋯
theorem
LO.Arith.Exponential.length_eq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(H : LO.Arith.Exponential x y)
:
theorem
LO.Arith.length_mul_pow2_add_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{p : V}
{b : V}
(pos : 0 < a)
(pp : LO.Arith.Pow2 p)
(hb : b < p)
:
theorem
LO.Arith.length_mul_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{p : V}
(pos : 0 < a)
(pp : LO.Arith.Pow2 p)
:
theorem
LO.Arith.pos_of_lt_length
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{b : V}
(h : a < ‖b‖)
:
0 < b
theorem
LO.Arith.le_log_of_lt_length
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{b : V}
(h : a < ‖b‖)
:
a ≤ LO.Arith.log b
theorem
LO.Arith.exponential_log_le_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{b : V}
(pos : 0 < a)
(h : LO.Arith.Exponential (LO.Arith.log a) b)
:
b ≤ a
theorem
LO.Arith.lt_exponential_log_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{b : V}
(h : LO.Arith.Exponential (LO.Arith.log a) b)
:
theorem
LO.Arith.lt_exp_len_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{b : V}
(h : LO.Arith.Exponential ‖a‖ b)
:
a < b
theorem
LO.Arith.le_iff_le_log_of_exp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
{a : V}
(H : LO.Arith.Exponential x y)
(pos : 0 < a)
:
y ≤ a ↔ x ≤ LO.Arith.log a
theorem
LO.Arith.le_iff_lt_length_of_exp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
{a : V}
(H : LO.Arith.Exponential x y)
:
theorem
LO.Arith.Exponential.lt_iff_log_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
{a : V}
(H : LO.Arith.Exponential x y)
(pos : 0 < a)
:
a < y ↔ LO.Arith.log a < x
theorem
LO.Arith.Exponential.lt_iff_len_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
{a : V}
(H : LO.Arith.Exponential x y)
:
theorem
LO.Arith.Exponential.le_of_lt_length
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
{a : V}
(H : LO.Arith.Exponential x y)
:
theorem
LO.Arith.Exponential.le_log
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(H : LO.Arith.Exponential x y)
:
x ≤ LO.Arith.log y
theorem
LO.Arith.Exponential.lt_length
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(H : LO.Arith.Exponential x y)
:
theorem
LO.Arith.lt_exponential_length
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{b : V}
(h : LO.Arith.Exponential ‖a‖ b)
:
a < b
theorem
LO.Arith.brange_exists_unique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
(x : V)
:
x < ‖a‖ → ∃! y : V, LO.Arith.Exponential x y
theorem
LO.Arith.exp_bexp_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : x < ‖a‖)
:
LO.Arith.Exponential x (LO.Arith.bexp a x)
theorem
LO.Arith.bexp_eq_zero_of_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : ‖a‖ ≤ x)
:
LO.Arith.bexp a x = 0
@[simp]
theorem
LO.Arith.bexp_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(x : V)
:
LO.Arith.bexp 0 x = 0
@[simp]
theorem
LO.Arith.exp_bexp_of_lt_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
:
LO.Arith.Exponential x (LO.Arith.bexp a x) ↔ x < ‖a‖
@[simp]
theorem
LO.Arith.bexp_le_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
(x : V)
:
LO.Arith.bexp a x ≤ a
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.bexp_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₂ LO.Arith.bexp via LO.FirstOrder.Arith.bexpDef
@[simp]
theorem
LO.Arith.bexp_defined_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.bexpDef) ↔ v 0 = LO.Arith.bexp (v 1) (v 2)
instance
LO.Arith.bexp_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₂ LO.Arith.bexp
Equations
- ⋯ = ⋯
instance
LO.Arith.instBounded₂Bexp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
LO.FirstOrder.Arith.Bounded₂ LO.Arith.bexp
Equations
- ⋯ = ⋯
theorem
LO.Arith.bexp_monotone_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{i : V}
{j : V}
(hi : i < ‖a‖)
(hj : j < ‖a‖)
:
LO.Arith.bexp a i < LO.Arith.bexp a j ↔ i < j
theorem
LO.Arith.bexp_monotone_le_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{i : V}
{j : V}
(hi : i < ‖a‖)
(hj : j < ‖a‖)
:
LO.Arith.bexp a i ≤ LO.Arith.bexp a j ↔ i ≤ j
theorem
LO.Arith.bexp_eq_of_lt_length
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{i : V}
{a : V}
{a' : V}
(ha : i < ‖a‖)
(ha' : i < ‖a'‖)
:
LO.Arith.bexp a i = LO.Arith.bexp a' i
@[simp]
theorem
LO.Arith.bexp_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : x < ‖a‖)
:
LO.Arith.Pow2 (LO.Arith.bexp a x)
@[simp]
theorem
LO.Arith.lt_bexp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : x < ‖a‖)
:
x < LO.Arith.bexp a x
@[simp]
theorem
LO.Arith.bexp_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : x < ‖a‖)
:
0 < LO.Arith.bexp a x
theorem
LO.Arith.lt_bexp_len
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : ‖x‖ < ‖a‖)
:
x < LO.Arith.bexp a ‖x‖
theorem
LO.Arith.bexp_eq_of_exp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{a : V}
{x : V}
(h : x < ‖a‖)
(H : LO.Arith.Exponential x y)
:
LO.Arith.bexp a x = y
theorem
LO.Arith.log_bexp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : x < ‖a‖)
:
LO.Arith.log (LO.Arith.bexp a x) = x
theorem
LO.Arith.len_bexp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{x : V}
(h : x < ‖a‖)
:
‖LO.Arith.bexp a x‖ = x + 1
@[simp]
@[simp]
theorem
LO.Arith.bexp_pos_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
(h : 0 < a)
:
LO.Arith.bexp a 0 = 1
theorem
LO.Arith.bexp_monotone
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a₁ : V}
{x₁ : V}
{a₂ : V}
{x₂ : V}
(h₁ : x₁ < ‖a₁‖)
(h₂ : x₂ < ‖a₂‖)
:
LO.Arith.bexp a₁ x₁ < LO.Arith.bexp a₂ x₂ ↔ x₁ < x₂
theorem
LO.Arith.bexp_monotone_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a₁ : V}
{x₁ : V}
{a₂ : V}
{x₂ : V}
(h₁ : x₁ < ‖a₁‖)
(h₂ : x₂ < ‖a₂‖)
:
LO.Arith.bexp a₁ x₁ ≤ LO.Arith.bexp a₂ x₂ ↔ x₁ ≤ x₂
theorem
LO.Arith.bexp_add
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x₁ : V}
{x₂ : V}
{a : V}
(h : x₁ + x₂ < ‖a‖)
:
LO.Arith.bexp a (x₁ + x₂) = LO.Arith.bexp a x₁ * LO.Arith.bexp a x₂
theorem
LO.Arith.bexp_two_mul
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{a' : V}
{x : V}
(hx : 2 * x < ‖a‖)
(hx' : x < ‖a'‖)
:
LO.Arith.bexp a (2 * x) = LO.Arith.bexp a' x ^ 2
theorem
LO.Arith.bexp_two_mul_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{i : V}
:
LO.Arith.bexp (2 * a) (i + 1) = 2 * LO.Arith.bexp a i
theorem
LO.Arith.bexp_two_mul_add_one_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{i : V}
:
LO.Arith.bexp (2 * a + 1) (i + 1) = 2 * LO.Arith.bexp a i
Equations
- LO.Arith.fbit a i = a / LO.Arith.bexp a i % 2
Instances For
@[simp]
theorem
LO.Arith.fbit_lt_two
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
(i : V)
:
LO.Arith.fbit a i < 2
@[simp]
theorem
LO.Arith.fbit_le_one
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
(i : V)
:
LO.Arith.fbit a i ≤ 1
theorem
LO.Arith.fbit_eq_one_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{i : V}
:
LO.Arith.fbit a i = 1 ↔ LO.Arith.LenBit (LO.Arith.bexp a i) a
theorem
LO.Arith.fbit_eq_zero_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{i : V}
:
LO.Arith.fbit a i = 0 ↔ ¬LO.Arith.LenBit (LO.Arith.bexp a i) a
theorem
LO.Arith.fbit_eq_zero_of_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{a : V}
{i : V}
(hi : ‖a‖ ≤ i)
:
LO.Arith.fbit a i = 0
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.fbit_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₂ LO.Arith.fbit via LO.FirstOrder.Arith.fbitDef
@[simp]
theorem
LO.Arith.fbit_defined_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.fbitDef) ↔ v 0 = LO.Arith.fbit (v 1) (v 2)
instance
LO.Arith.fbit_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₂ LO.Arith.fbit
Equations
- ⋯ = ⋯
instance
LO.Arith.instBounded₂Fbit
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
LO.FirstOrder.Arith.Bounded₂ LO.Arith.fbit
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.fbit_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(i : V)
:
LO.Arith.fbit 0 i = 0
@[simp]
theorem
LO.Arith.fbit_mul_two_mul
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
(i : V)
:
LO.Arith.fbit (2 * a) (i + 1) = LO.Arith.fbit a i
@[simp]
theorem
LO.Arith.fbit_mul_two_add_one_mul
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
(i : V)
:
LO.Arith.fbit (2 * a + 1) (i + 1) = LO.Arith.fbit a i
@[simp]
theorem
LO.Arith.fbit_two_mul_zero_eq_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
:
LO.Arith.fbit (2 * a) 0 = 0
@[simp]
theorem
LO.Arith.fbit_two_mul_add_one_zero_eq_one
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(a : V)
:
LO.Arith.fbit (2 * a + 1) 0 = 1
@[simp]
theorem
LO.Arith.log_exponential
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
:
LO.Arith.log (exp a) = a
theorem
LO.Arith.exp_log_le_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
(pos : 0 < a)
:
exp LO.Arith.log a ≤ a
theorem
LO.Arith.lt_two_mul_exponential_log
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
(pos : 0 < a)
:
a < 2 * exp LO.Arith.log a
theorem
LO.Arith.log_mul_exp_add_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
{b : V}
(pos : 0 < a)
(i : V)
(hb : b < exp i)
:
LO.Arith.log (a * exp i + b) = LO.Arith.log a + i
theorem
LO.Arith.log_mul_exp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
(pos : 0 < a)
(i : V)
:
LO.Arith.log (a * exp i) = LO.Arith.log a + i
theorem
LO.Arith.exp_le_iff_le_log
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{a : V}
(pos : 0 < a)
:
exp i ≤ a ↔ i ≤ LO.Arith.log a