So I’m self-learning coq. And I came across the proof for associativity in addition `forall (a b c : nat)`

Appearntly when we do `induction a.`

after `intros a b c.`

, it creates 2 subgoals

and afterwards we simply need to show that the two sides in both subgoals are equivalent, and the proof is completed.

So I’m just wondering why we don’t need to do `induction b.`

and `induction c.`

to complete the proof? Why only performing induction on `a`

is able to complete the proof?

Or in other words, how come in the function that returns the proof, we just get `b`

and `c`

for “free”? Constructively don’t we need something like a double induction applied twice?