English
For all x and n, appr(x,n) < p^n.
Русский
Для всех x и n выполняется apr(x,n) < p^n.
LaTeX
$$$0 \le \operatorname{appr}(x,n) < p^n$$$
Lean4
theorem appr_lt (x : ℤ_[p]) (n : ℕ) : x.appr n < p ^ n := by
induction n generalizing x with
| zero => simp only [appr, _root_.pow_zero, zero_lt_one]
| succ n
ih =>
simp only [appr, map_natCast, ZMod.natCast_self, RingHom.map_pow, Int.natAbs, RingHom.map_mul]
have hp : p ^ n < p ^ (n + 1) := by apply Nat.pow_lt_pow_right hp_prime.1.one_lt n.lt_add_one
split_ifs with h
· apply lt_trans (ih _) hp
· calc
_ < p ^ n + p ^ n * (p - 1) := ?_
_ = p ^ (n + 1) := ?_
· apply add_lt_add_of_lt_of_le (ih _)
apply Nat.mul_le_mul_left
apply le_pred_of_lt
apply ZMod.val_lt
· rw [mul_tsub, mul_one, ← _root_.pow_succ]
apply add_tsub_cancel_of_le (le_of_lt hp)
