Adding 1 is the successor
Step by step one goes far. – Dutch proverb
To solve this one you will need to remember that the number 1 is
defined to be the successor of 0. It’s a nice short proof and a break
from using induction, but you may have to use the “More” menu to find
the fact that 1 = succ 0, which is our definition of 1.
Proving: ℕ n ⇒ succ n = n + 1
An error occurred executing the proof.
View the workspace as text to see steps not executed.
For safety this worksheet is read-only.
[1]ℕ n and succ n = n + 1 ⇒ succ n = n + 1 starting proof of ℕ n ⇒ succ n = n + 1
Selection
Will you kindly help advance Prooftoys usability
by enabling detailed tracing of your usage?
You can opt out at any time.
For more information, see the
privacy information page.
Basic
Tactics
More
Descriptions
Edit
Rewrites and other often-used actions. (☆ means the selected term.)
assume (A ⇒ A)
assume explicitly (A ⇒ A)
check a tautology
check a tautology instance
consider a term to transform (A = A)
look up a fact