# Zulip Chat Archive

## Stream: new members

### Topic: How to show 2 \ne 1?

#### Daniel Fabian (May 26 2020 at 17:59):

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 (May 26 2020 at 17:59):

`norm_num`

?

#### Johan Commelin (May 26 2020 at 17:59):

`exact dec_trivial`

?

#### Daniel Fabian (May 26 2020 at 18:00):

`norm_num`

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

#### Kevin Buzzard (May 26 2020 at 18:01):

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

#### Alex J. Best (May 26 2020 at 18:01):

`norm_num`

should close both of those goals.

#### Kevin Buzzard (May 26 2020 at 18:01):

right

#### Kevin Buzzard (May 26 2020 at 18:02):

```
import tactic data.int.modeq
example : ¬(2 : ℤ) ∣ 1 :=
begin
norm_num,
end
example : ¬(2 : ℕ) ∣ 1 :=
begin
norm_num
end
```

works fine

#### Daniel Fabian (May 26 2020 at 18:03):

ah, I didn't know about `modeq`

.

#### Alex J. Best (May 26 2020 at 18:04):

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 (May 26 2020 at 18:05):

cool, thanks.

Last updated: May 14 2021 at 12:18 UTC