2 subgoals x, y : nat H : x + 0 = y + 0
but after that I don't know how to to get rid of 0 in H.
2 subgoals x, y : nat H : x + 0 = y + 0
but after that I don't know how to to get rid of 0 in H.
It's true that on paper you would simply conclude because x + 0 = x
. Well, in Coq you have to prove it because addition is left-biased (it computes by looking up its first argument).
I would suggest proving first that
forall n, n + 0 = n
I would go with something like this:
Theorem ex9: forall x y n, x + n = y + n -> x = y.
Proof.
intros.
induction n as [| n' IH].
- rewrite add_0_r in H. (* replace x + 0 with x *)
rewrite add_0_r in H. (* replace y + 0 with y *)
assumption.
- apply IH. (* replace x=y with x+n' = y+n' *)
rewrite <- plus_n_Sm in H. (* replace x + S n' with S (x + n') *)
rewrite <- plus_n_Sm in H. (* replace y + S n' with S (y + n') *)
apply S_injective in H. (* drop both S constructors *)
assumption.
Qed.