zero_add
0 + n = n for all natural numbers n
? 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 / 2
0%
MCQ · TACTIC RECOGNITION
0 + n = n for all natural numbers n
Question 1 of 2
Which single tactic closes the base case goal `0 + 0 = 0`?
A) simp [Nat.add_zero]
B) rfl
C) ring
D) induction n