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

State before:
c : ℕ
⊢ c < (2 ^ c - 1).succ.divisors.card
Tactic:
rw [Nat.succ_eq_add_one, Nat.sub_add_cancel Nat.one_le_two_pow,
Nat.divisors_prime_pow Nat.prime_two, card_map, card_range, Nat.lt_succ_iff]
State after:
no goals