Theorem rsucc-02

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: dist-split, s, ls,
• Comment:
• Used by: addle-01, dist, eq, modeq, mult-a, mult-c, numeral-10, numeral-17, rdist, rsucc, rsucc-01, succ, three, threeeq, threels, two-succ-03, two-succ-04, twols-01, zero, zero-01, zero-03,
• Used by units in proved state: nat-prime, nat-pot, nat-div, intnat, nat-pair, nat-even, int-pair,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 1
• Used lemmas: mult-rec,
• Used spec theorems:
  • Used simplifier rules:
    • nat-basic/succ