Why 0 + n = n needs induction
n + 0 is rfl, 0 + n is not. See what computation does and does not give you.
0/6 completed in this course
Lean workspaceWrite only the proof steps. The theorem above is fixed.
Enter after constructor adds both goal bulletsLoading editor…
Type
\to, \and, \< … to insert symbols while typingNo problems detected so far. Run a check to hear from Lean.
ReadyLn 1, Col 1Pre-check passedLean 4