Simple question about arithmitic

Stream: new members

[HenrikT]

Hi, i am trying to rewrite some terms to show that they are equal, however i fail to find how to do it.

I am trying to rewrite P x (n1 + 1 + a) y z into P x (n1 + Nat.succ a) y z
The implementation of P should be irrelevant for this
I have a similar problem when trying to show that n = m+(n-m) with (m < n), n m are Integers
Any ideas on which rules i can use for that ?

Is there a similar auto solver like tauto but for such simple arithmetic questions ?

Thanks in advance :D

[Damiano Testa]

I suspect that

  rw [add_assoc, add_comm 1, Nat.succ_eq_add_one]

might work (untested).

[HenrikT]

ok, thanks that worked.

In the second case however how can i resolve that, as subtraction is not associative.
I also cannot rw the term to n = n + (-m + m) as -m is not an integer
Any ideas ?

[Damiano Testa]

Does docs#Nat.add_sub_assoc exits? [EDIT: it seems so, it may be what you want!]

[Damiano Testa]

Note that there is also docs#Nat.add_sub_cancel'. If you posted a #mwe, it would be easier to know what can be useful.

[HenrikT]

there isn't much of a #mwe but what i am trying to proof is the following:
theorem existsAEqualizingLt (n m : ℕ) : m < n → ∃ a, n = m + a := by sorry

Edit: Thank you for your help docs#Nat.add_sub_cancel' did the joy :D

FYI: the proof looks as follows:

theorem existsAEqualizingLt (n m : ℕ) : m < n → ∃ a, n = m + a := by
  intro h
  use (n-m)
  rw [Nat.add_sub_cancel']
  rw [Nat.lt_iff_le_and_ne] at h
  exact h.1

[Damiano Testa]

In case you are curious about how to use the available results, you can also prove your theorem using docs#exists_add_of_le:

import Mathlib.Data.Nat.Order.Basic

theorem existsAEqualizingLt (n m : ℕ) : m < n → ∃ a, n = m + a := by
  intro h
  exact exists_add_of_le h.le

and, in fact, the whole proof can be shortened to

theorem existsAEqualizingLt (n m : ℕ) : m < n → ∃ a, n = m + a :=
fun h ↦ exists_add_of_le h.le