If there are common terms in the LHS and RHS of a goal while in proof mode, is it possible to remove them?
Example a : forall (n m : nat), (S m) + (n + m) = (S m) + (m + n). Proof. intros.
when the goal becomes:
S m + (n + m) = S m + (m + n)
Is there a way to remove the
S m that is common in both LHS and RHS to make it just
(n + m) = (m + n)
Yes, you can use the
f_equal made it
n + m = m + n
Ju-sh has marked this topic as resolved.
You can also use
congr (S m + _)
congr only available for use with ssreflect?
Indeed, vanilla Coq's
congruence would only work if removing the common term solves the goal.
Last updated: Sep 23 2023 at 06:01 UTC