## Stream: Coq users

### Topic: Proving forall (n m: nat), n = m + (n - m).

#### Jerome Hugues (Apr 25 2023 at 14:57):

Hi,

As part of my development, I need to prove the following:
`Lemma foo: forall (n m: nat), n = m + (n - m).`

This is problematic with the current definition of "-" for `Nat` and the order of operations.

I wonder if there is another definition of natural numbers that would help working-around this.
One solution is to do the proof in Z of course, but that creates other issues like adding additional predicates in other places.

Thanks!

#### Pierre Jouvelot (Apr 25 2023 at 15:05):

You can look at what is done in `nat.v`, part of the Mathematical Components library (https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssrnat.html). This lemma (`subnKC`) is only true if the additional condition `m <= n` is added.

#### Jerome Hugues (Apr 25 2023 at 15:35):

Indeed, adding `m <= n` makes this lemma trivial with `lia`. But I was looking for a more general solution without this extra hypothesis.

#### Pierre Castéran (Apr 25 2023 at 15:44):

Jerome Hugues said:

Indeed, adding `m <= n` makes this lemma trivial with `lia`. But I was looking for a more general solution without this extra hypothesis.

Indeed, the considered equality is equivalent to this hypothesis.

``````Lemma foo: forall (n m: nat), n = m + (n - m) <-> m <= n.
Proof. intros; lia. Qed.
``````

#### Paolo Giarrusso (Apr 25 2023 at 15:48):

I wonder if there is another definition of natural numbers that would help working-around this.

if you're just changing minus, I think not: take `n = 0, m = 1`, we search `X := minus' n m` such that `n = m + X`, that is `0 = 1 + X`. But `X := -1` is the unique solution for that equation

#### Guillaume Melquiond (Apr 25 2023 at 15:58):

Jerome Hugues said:

`Lemma foo: forall (n m: nat), n = m + (n - m).`
One solution is to do the proof in Z of course

That is worse than that. If you look at the instance `(foo 0)`, it actually states `forall m, 0 = m + (0 - m)`. In other words, any element has an inverse for addition, which precisely characterizes the difference between `nat` and `Z`. So, it is not just that you could do the proof in `Z`; you have to do the proof in `Z` (or any superset).

Last updated: Oct 04 2023 at 23:01 UTC