succ_ne_zero
For all n : ℕ, succ(n) ≠ 0
? MCQ
+10 XP
Tactic Recognition
Pick the right move. No typing required.
🔒 BUILD
+25 XP
Fill in the Proof
Type the missing tactics into the skeleton.
Complete MCQ first to unlock
🔒 TRACE
+50 XP
Expert Auditor
Justify every decision. Earns the most XP.
Complete Build first to unlock
🔒 REVIEW
+20 XP
Spot the Issues
Find what's wrong with this bloated proof.
Complete Build first to unlock
Q1 / 1
0%
MCQ · TACTIC RECOGNITION
For all n : ℕ, succ(n) ≠ 0
Question 1 of 1
Which tactic is most appropriate to progress succ_ne_zero?
A) simp
B) ring
C) omega
D) by_cases h