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
c for “free”? Constructively don’t we need something like a double induction applied twice?