# Zulip Chat Archive

## Stream: new members

### Topic: How to prove 0 \neq 1 ?

#### leafGecko (Aug 11 2021 at 11:23):

Dear all,

I am attempting the finale part of Natural Number Game, where I am trying to proof `theorem not_succ_le_self (a : mynat) : ¬ (succ a ≤ a)`

. It eventually boils down to prove `H: 0 eq 1`

implies false, and I find myself stuck. Any help would be greatly appreciated!

#### Kevin Buzzard (Aug 11 2021 at 11:24):

Although it's probably not the official way to do it, you can probably prove `0 != 1`

with `intro h, cases h`

.

#### leafGecko (Aug 11 2021 at 11:29):

Kevin Buzzard said:

Although it's probably not the official way to do it, you can probably prove

`0 != 1`

with`intro h, cases h`

.

`intro H', cases H'`

yields

```
c' : mynat,
Hc : 0 = 1 + c' → false,
H' : 0 = 1 + succ c'
⊢ false
```

May I know what to do next?

#### Anne Baanen (Aug 11 2021 at 11:42):

Could you give the full proof you have until now?

#### Kevin Buzzard (Aug 11 2021 at 11:42):

I claim that your goal was not "0 != 1" then!

#### leafGecko (Aug 11 2021 at 11:43):

Oops sorry! I mistake the 2nd goal for the current goal... `intro h, cases h`

do solve the goal then.

#### Kyle Miller (Aug 11 2021 at 17:41):

I'm not sure if it's available in the natural number game, but I learned about the `contradiction`

tactic recently:

```
example (n : ℕ) : 0 ≠ 1 + n.succ :=
begin
contradiction,
end
```

You can also use `trivial`

, which tries `contradiction`

.

#### Mario Carneiro (Aug 11 2021 at 17:44):

I think `contradiction`

is also a grab bag of strategies; the one that is doing the work here is `injection`

, which is just a special case of the `cases`

tactic

Last updated: Dec 20 2023 at 11:08 UTC