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

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