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

Stream: Is there code for X?

[Jakob Scholbach]

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]

The version with <= conditions exists.

[Markus Himmel]

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

[Johan Commelin]

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

[Eric Wieser]

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]

But it's often more convenient to work in terms of n.succ instead of 0 < n

[Johan Commelin]

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]

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]

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

[Jakob Scholbach]

@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]

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]

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