a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < ↑a
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ≤ ↑a ^ 2 - (↑a - 1) ^ 2 - 1
rw [sub_sq, mul_one, one_pow, sub_add, sub_sub_cancel, two_mul, sub_sub, ← add_sub,
  le_add_iff_nonneg_right, sub_nonneg, Int.add_one_le_iff]
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < a
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < ↑a
norm_cast
no goals
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < a
exact lt_of_le_of_lt (Nat.succ_le_of_lt (Nat.pos_of_ne_zero hy0)) hya
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ ↑a ^ 2 - (↑a - 1) ^ 2 - 1 ≤ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ^ 2 - (↑a - 1) ^ 2 - 1 ≤ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1
have := hya.le
no goals
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ ↑a ^ 2 - (↑a - 1) ^ 2 - 1 ≤ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1
mono * <;> norm_cast <;> simp [Nat.zero_le, Nat.succ_le_of_lt (Nat.pos_of_ne_zero hy0)]
no goals
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1 = 2 * ↑a * ↑y - ↑y * ↑y - 1
ring