English
The sequence y_n(a) is strictly increasing in n: y_n < y_{n+1} for all n.
Русский
Последовательность y_n(a) строго возрастает по n: y_n < y_{n+1} для всех n.
LaTeX
$$$\\text{StrictMono}(y^{(a)})$, i.e., $y^{(a)}_n < y^{(a)}_{n+1}$ for all n.$$
Lean4
theorem strictMono_y : StrictMono (yn a1)
| _, 0, h => absurd h <| Nat.not_lt_zero _
| m, n + 1, h =>
by
have : yn a1 m ≤ yn a1 n :=
Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_y hl) fun e => by rw [e]
simp only [yn_succ, gt_iff_lt]; refine lt_of_le_of_lt ?_ (Nat.lt_add_of_pos_left <| x_pos a1 n)
rw [← mul_one (yn a1 m)]
exact mul_le_mul this (le_of_lt a1) (Nat.zero_le _) (Nat.zero_le _)
