induction - Coq で n + S m = S (n + m) を証明する方法

Question

それで、「計算論理入門」スクリプトを使って Coq を学ぼうとしていて、練習問題が与えられました。「forall ab, 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.

最後のサブゴールは単なる nat であり、どうすればよいかまったくわかりません。