Как доказать n + S m = S (n + m) в Coq

Итак, я пытаюсь изучить Coq, используя сценарий «Введение в вычислительную логику», и мне дали упражнение. Это доказать следующее: «для всех a b, a + S b = S (a + b)». Мне дано определение "nat_ind":

  (p : nat -> Prop)
  (basis : p 0)
  (step : forall n, p n -> p (S n)) :
    forall n, p n := fix f n :=
      match n return p n with
      | 0 => basis
      | S n => step n (f n)
      end.

У меня была попытка сделать это, и я решил проблему с помощью этого метода, и он сработал:

intros a b. revert a.
  apply (nat_ind(fun a => a + S b = S (a+b))); simpl.
  -reflexivity.
  -intros. f_equal. exact H.

Проблема возникает теперь, когда я должен решить ту же проблему, но мне нужно немедленно применить лемму индукции и я не могу использовать вступления или тактику индукции, прежде чем я это сделаю. Как мне это сделать?

Я попытался удалить первую строку из своей первой попытки, но выдает ошибку: «Ссылка b не найдена в текущей среде».

Обновление: я кое-что получил. Это мой текущий код:

Goal forall a b, a + S b = S (a + b).
Proof. 
  apply nat_ind.
  - intros a b. revert a. 
    apply (nat_ind (fun a => a + S b = S (a + b)));simpl.
      + reflexivity.
      + intros.  f_equal. exact H.
  -intros. revert a. apply (nat_ind (fun a => a + S b = S (a + b))); simpl.
    + reflexivity.
    + intros. f_equal. exact H0.

Последняя подцель просто естественна, и я вообще не знаю, как ее решить.