0 != 1

Stream: new members

[King Crawford]

Hello everyone. I am looking for a tactic I can use to prove that nat 0 != 1 but surprisingly could not find one by googling. Appreciate the help.

[Adam Topaz]

Here are a few methods:

import tactic

example : 0 ≠ 1 := zero_ne_one

example : 0 ≠ 1 := by norm_num

example : 0 ≠ 1 := dec_trivial

example : 0 ≠ 1 .

[Adam Topaz]

In general we have a list of tactics on the community webpage: tactic#norm_num as an example

[Michael Stoll]

I first read the title as 0! = 1 (which is also true...). :smile: