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

State before:
⊢ 12 < 14
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
h : 6 ≤ n
h0 : 2 * n < g n
⊢ 2 * (n + 1) < g (n + 1)
Tactic:
rw [Nat.mul_succ, g_succ]
State after:
n : ℕ
h : 6 ≤ n
h0 : 2 * n < g n
⊢ 2 * n + 2 < g n + n.succ.divisors.card

State before:
n : ℕ
h : 6 ≤ n
h0 : 2 * n < g n
⊢ 2 * n + 2 < g n + n.succ.divisors.card
Tactic:
exact add_lt_add_of_lt_of_le h0 <| two_le_card_divisors <|
  Nat.succ_le_succ (Nat.one_le_of_lt h)
State after:
no goals