How to prove 0 \neq 1 ?

Stream: new members

[leafGecko]

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]

Although it's probably not the official way to do it, you can probably prove 0 != 1 with intro h, cases h.

[leafGecko]

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]

Could you give the full proof you have until now?

[Kevin Buzzard]

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

[leafGecko]

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

[Kyle Miller]

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]

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