add_comm.v

(* NOTE: S means successor. So, "S a" means successor of a (aka a+1) *)
Lemma S_add_left :
  forall (a b : nat),
  S (a + b) = a + S b. (* This is the proposition, given as a type. This is the type signature for the lemma *)
Proof.
  (* I am using the tactic language here. Internally this generates an expression that has the type above *)
  intros. (* Bring the variables a and b into scope *)
  destruct a  (* "destruct" is similar to induction, but it does not give you an inductive hypothesis *)
    ; easy. (* "easy" is a builtin tactic that can solve very simple proof goals. The semicolon means to apply it to all subgoals generated by the previous command *)
Qed.

Print S_add_left. (* Stepping to this line will print the expression generated by my tactic-based proof for S_add_left *)

Theorem thm :
  forall (a b : nat),
  (a + b) = (b + a).
Proof.
  intros.
  induction a; try easy. (* "try easy" means that if easy fails, don't give up on the entire proof. Just keep the subgoals that remain to be solved later *)
  simpl. (* Simplify the expression by doing basic computation *)
  rewrite IHa. (* Rewrite the current goal using the equation IHa from the hypothesis. This equation is the inductive hypothesis *)
  simpl.
  rewrite S_add_left. (* Use the equation from the lemma given at the start of the file to rewrite the current goal *)
  reflexivity. (* After all that rewriting, the two sides of the equality are now syntactically identical, so we can apply reflexivity to finish the the subgoal *)
Qed. (* That was the last subgoal, so we are done! *)