a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ < (fun x x_1 => x * x_1) k x✝
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ ∀ (x : ℕ), succ seed ≤ x → P x → x < (fun x x_1 => x * x_1) k x
intro _ hl _
case h.e'_3
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ < (fun x x_1 => x * x_1) k x✝
convert (mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
no goals
case h.e'_3
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝
rw [one_mul]