Theorem: IMOSL.IMO2006N3.f_succ_lt_self_of_succ_prime_large (IMOSLLean4/IMO2006/N3/N3.lean)

State before:
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ f n.succ < f n
Tactic:
apply f_lt_f_of_g
State after:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ g n.succ * n < g n * n.succ

State before:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ g n.succ * n < g n * n.succ
Tactic:
rw [g_succ, card_divisors_prime h0, add_mul, Nat.mul_succ, add_lt_add_iff_left]
State after:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ 2 * n < g n

State before:
case h
n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
⊢ 2 * n < g n
Tactic:
exact two_mul_lt_g n h
State after:
no goals