Stream: Coq users

Topic: How to prove statement?


view this post on Zulip sara lee (Oct 19 2021 at 06:19):

n:nat
H : S n > 0
Goal: 1 = S n

view this post on Zulip Théo Winterhalter (Oct 19 2021 at 06:40):

S n > 0 is always true, but 1 = S n is only true when n = 0.
You probably should read more on the representation of natural numbers if this is not clear to you.
But basically, S n represents 1 + n.


Last updated: Feb 01 2023 at 11:04 UTC