How to show 2 \ne 1?

Stream: new members

[Daniel Fabian]

I've come across an embarrassingly simple problem:

example : ¬(2 : ℤ) ∣ 1 :=
begin
    intro h,
    have : (2 : ℤ) = 1 := int.eq_one_of_dvd_one (show (0 : ℤ) ≤ 2, by simp) h,
    cases this,
end

example : ¬(2 : ℕ) ∣ 1 :=
begin
    rw nat.dvd_one,
    intro,
    cases a,
end

Due to the local context in my proof, lean wanted me to show the first version (in integers as opposed to natural numbers) and the number of theorems available is substantially smaller. Is there a way to cast the statement down to naturals (even though it's technically a weaker statement, so I might have to prove that 2 and 1 are indeed \ge 0).

And secondly, how do I convince lean that something is impossible, i.e. how do I apply refl in a negative position? Looks like adding it as an assumption and then definition by cases eliminated it.

Also, library_search came up with the idea to call decidable prop on the proposition and use that instead: exact of_to_bool_ff rfl

Is introducing followed by cases the right way to discharge a non-equality proof?

[Johan Commelin]

norm_num?

[Johan Commelin]

exact dec_trivial?

[Daniel Fabian]

norm_num didn't do the trick, because it left everything in integer domain.

[Kevin Buzzard]

Do I need an import for this? Lean is complaining about has_dvd int

[Alex J. Best]

norm_num should close both of those goals.

[Kevin Buzzard]

right

[Kevin Buzzard]

import tactic data.int.modeq

example : ¬(2 : ℤ) ∣ 1 :=
begin
  norm_num,
end

example : ¬(2 : ℕ) ∣ 1 :=
begin
  norm_num
end

works fine

[Daniel Fabian]

ah, I didn't know about modeq.

[Alex J. Best]

If the question is how to reduce the first to the second (and not use norm_num, which really is the recommended way) you can do:

example : ¬(2 : ℤ) ∣ 1 :=
begin
    exact_mod_cast (_ : ¬ (2∣ 1)),
    rw nat.dvd_one,
    intro,
    cases a,
end

[Daniel Fabian]

cool, thanks.