Nat.sub_lt_sub_right

Stream: new members

[Scott Kovach]

I think mathlib is missing this lemma? if it's desired, I can change it to not depend on the ordered monoid lemmas (or maybe it really belongs in that setting?)

import Mathlib.Tactic

theorem Nat.sub_lt_sub_right : ∀ {k m n : Nat}, k < n → m < n → m - k < n - k
  | 0, _, _, _, h2 => h2
  | k+1, 0, n, h1, _ => by
    simp only [ge_iff_le, Nat.zero_le, tsub_eq_zero_of_le, tsub_pos_iff_lt, h1]
  | k+1, m+1, n+1, h1, h2 => by
    rw [Nat.add_sub_add_right, Nat.add_sub_add_right]
    exact Nat.sub_lt_sub_right (Nat.lt_of_succ_lt_succ h1) (Nat.lt_of_succ_lt_succ h2)

[Alex J. Best]

Loogle for ⊢ ?m - ?k < ?n - ?k finds docs#tsub_lt_tsub_right_of_le, which I believe will apply for nats.
https://loogle.lean-lang.org/?q=%E2%8A%A2+%3Fm+-+%3Fk+%3C+%3Fn+-+%3Fk

I guess this isn't quite the same though!

[Scott Kovach]

thanks for the reminder to try loogle! this lemma does have a stronger hypothesis, but this doesn't matter where I'm using it