Theorem: two_not_cube (FltRegular/FltThree/Primes.lean)

State before:
r : ℕ
⊢ r ^ 3 ≠ 2
Tactic:
apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono three_ne_zero).monotone 1 <;> norm_num
State after:
no goals