## 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

You can also use trivial, which tries contradiction.
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