a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < yn a1 (n + 1)
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ yn a1 m < yn a1 (n + 1)
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]
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < yn a1 (n + 1)
simp
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n * a
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a
refine' lt_of_le_of_lt _ (Nat.lt_add_of_pos_left <| x_pos a1 n)
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n * a
rw [← mul_one (yn a1 m)]
no goals
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a
exact mul_le_mul this (le_of_lt a1) (Nat.zero_le _) (Nat.zero_le _)
no goals
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ yn a1 m ≤ yn a1 n
rw [e]