p : ℕ
h : 0 < p
⊢ 0 < 2 ^ p - 1
p : ℕ
h : 0 < p
⊢ 0 < mersenne p
dsimp [mersenne]
no goals
p : ℕ
h : 0 < p
⊢ 0 < 2 ^ p - 1
calc
  0 < 2 ^ 1 - 1 := by norm_num
  _ ≤ 2 ^ p - 1 := Nat.sub_le_sub_right (Nat.pow_le_pow_of_le_right (Nat.succ_pos 1) h) 1
no goals
p : ℕ
h : 0 < p
⊢ 0 < 2 ^ 1 - 1
norm_num