If there are common terms in the LHS and RHS of a goal while in proof mode, is it possible to remove them?

As in:

```
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`

tactic.

Thanks!

Using `f_equal`

made it

```
n + m = m + n
```

Ju-sh has marked this topic as resolved.

You can also use `congr (S m + _)`

Is `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