peano arithmetic proof in fitch

Question

I've been tasked with proving that any natural number times the successor of zero is equal with that natural number. I've been trying to solve this problem using induction in the Fitch proof system, but I keep running into problems when I try and complete the proof. More specifically, I get the message "this sentence is of the wrong form," which I assume refers to the step I've cited as the basis case - but I can't figure out why it's of the wrong form and what the right form would be. It is also very possible that my understanding of how to do proofs by induction is mistaken. So if anyone could tell me what's wrong with the proof below, I would be grateful.

Answer 1

Your proof is fine! I think you just need to type out the goal on line 18.

Also note that you really don't need a proof by contradiction inside the Inductive Step: you can just take lines 8 through 14 and put them right after line 6, and get rid of lines 7, 15, 16, and 17.

Also, line 11 is exactly the same as line 10, so line 11 can be removed as well (and for line 13 just refer to line 10 instead of line 11)