# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: For naturals m < m', there is a positive integer s.th....

#### Jakob Scholbach (Apr 12 2021 at 09:28):

Is this in mathlib?

```
lemma sub_diff (m m' : ℕ) (h : m < m') : ∃ s : ℕ, 0 < s ∧ m' = m + s :=
begin
use m' - m,
split,
{ omega },
{ exact (nat.add_sub_of_le (le_of_lt h)).symm }
end
```

#### Johan Commelin (Apr 12 2021 at 09:33):

The version with `<=`

conditions exists.

#### Markus Himmel (Apr 12 2021 at 09:33):

There is docs#nat.exists_eq_add_of_lt which is similar to what you are looking for

#### Johan Commelin (Apr 12 2021 at 09:34):

I was thinking of https://leanprover-community.github.io/mathlib_docs/algebra/ordered_monoid.html#le_iff_exists_add

#### Eric Wieser (Apr 12 2021 at 09:35):

That golfs to

```
lemma nat.exists_eq_add_of_lt' (m m' : ℕ) (h : m < m') : ∃ s : ℕ, 0 < s ∧ m' = m + s :=
let ⟨k, hk⟩ := nat.exists_eq_add_of_lt h in ⟨k.succ, k.zero_lt_succ, hk⟩
```

#### Eric Wieser (Apr 12 2021 at 09:36):

But it's often more convenient to work in terms of `n.succ`

instead of `0 < n`

#### Johan Commelin (Apr 12 2021 at 09:38):

That's often true locally, but if you want to apply results in a different part of the library, then `0 < n`

is typically more flexible.

#### Johan Commelin (Apr 12 2021 at 09:39):

Because then you're often just handed a `n : nat`

, and you don't want to case on it before applying a lemma.

#### Eric Wieser (Apr 12 2021 at 09:48):

Worth PR'ing the above, perhaps as `nat.exists_eq_add_nonneg_of_lt`

then?

#### Jakob Scholbach (Apr 12 2021 at 11:20):

@Eric Wieser : OK, -- I'm in the middle of a PR #6743 in which I need this. Is it better to keep PRs affecting such fundamental files such as `algebra.ordered_monoid`

separate or could I just as well edit `algebra.ordered_monoid`

in the course of that PR #6743?

#### Eric Wieser (Apr 12 2021 at 11:32):

I'd recommend:

- adding the lemma wherever is most convenient for now, and continuing the PR - putting it in the right place right now will make your builds very slow
- creating a new PR with just that lemma, in the right place

By the time the first complex PR is close to ready to merge, chances are the second one is already merged, and all you have to do is remove your copy of the lemma

#### Yury G. Kudryashov (Apr 12 2021 at 20:08):

I usually put lemma into correct files and use `--old`

.

Last updated: May 17 2021 at 16:26 UTC