odd prime at least three

Stream: Is there code for X?

[Will Midwood]

Hi all,

Just wondering if there exists a proof for
nat.prime p ∧ odd p → 3 ≤ p

Thank you!

[Yakov Pechersky]

import data.nat.prime
import data.nat.parity

example {p : ℕ} (h : nat.prime p ∧ odd p) : 3 ≤ p :=
nat.succ_le_of_lt (lt_of_le_of_ne h.left.two_le (λ H, nat.odd_iff_not_even.mp h.right (H ▸ even_two))

[Kyle Miller]

The term mode proof is fine, but I wanted to see what's going on better, so here's a tactic proof:

import data.nat.prime
import data.nat.parity

example {p : ℕ} (hp : nat.prime p) (hodd : odd p) : 3 ≤ p :=
begin
  rw [nat.odd_iff_not_even, hp.even_iff, eq_comm] at hodd,
  rw [nat.succ_le_iff],
  exact lt_of_le_of_ne hp.two_le hodd,
end

[Kyle Miller]

It seems like we're missing a nat.succ_le_iff_le_and_ne lemma, which is what the last two lines are doing.

[Yaël Dillies]

docs#order.succ_le_iff + docs#lt_iff_le_and_ne

[Will Midwood]

Thanks all! I didn't realise that nat.succ_le_ifff would automatically decrement 3 to 2. Handy trick!

[Michael Stoll]

There is docs#nat.prime.five_le_of_ne_two_of_ne_three, which makes me wonder why there is no similar statement for 3...

[Michael Stoll]

docs#nat.prime.even_iff could also be used in the proof.