The Coq mailing list

[Yong Luo <yong.luo AT durham.ac.uk>]

Dear all,

I am stuck in proving 1 /= 0, ie. one is not equal to zero, ~ (S O) =
O, where 1 and 0 are Natural Numbers, nat.

I can find any similar proposition in Coq's library of classical logic.

Can anyone give me a hand and tell me how to prove it in Coq?

Thank you.

Yong