lemma to convert goal from `A ≥ B` to `A - B ≥ 0` ?

Stream: new members

[rzeta0]

Is there a lemma for converting a goal of the form A ≥ B to A - B ≥ 0 ?

Or to 0 ≤ A - B.

[Johan Commelin]

I hope there is something called docs#sub_nonneg ...

[Johan Commelin]

Sorry, need to run

[rzeta0]

Thanks - that looks. promising!

I made up a minimal example and tried both sub_nonneg and le_of_sub_nonneg - sadly I am a beginner and might not be using the right syntax to transform the goal, hence the following gives errors

import Mathlib.Tactic

example : ∃ n: ℕ, ∃ m: ℕ, m ≤ n := by
  -- goal is ∃ n m, m ≤ n
  apply sub_nonneg -- prefer goal 0 ≤ n - m
  sorry

example : ∃ n: ℕ, ∃ m: ℕ, m ≤ n := by
  -- goal is ∃ n m, m ≤ n
  apply le_of_sub_nonneg -- prefer goal 0 ≤ n - m
  sorry

the errors are:

tactic 'apply' failed, failed to unify
  0 ≤ ?a - ?b ↔ ?b ≤ ?a
with
  ∃ n m, m ≤ n
⊢ ∃ n m, m ≤ n

tactic 'apply' failed, failed to unify
  ?b ≤ ?a
with
  ∃ n m, m ≤ n
⊢ ∃ n m, m ≤ n

[cairunze cairunze]

here you need to produce some evidence, so we could do the use tactic.

example : ∃ n: ℕ, ∃ m: ℕ, m ≤ n := by
  use 0,0

the rest is actually taken care of automatically.

For the original question, i guess we could always try

example : m ≤ n ↔ m - n ≤ 0 := by
  /-
  Try this: exact Iff.symm tsub_nonpos
  -/
  apply?
  sorry

but this probably depends on the type of m and n (they are assumed to be \N if not specified).

[rzeta0]

Thanks @cairunze cairunze

I am actually asking about how to change the current goal. The example was just to illustrate, and as you say can be done more simply.

How does one apply a lemma/theorem to the goal?

[cairunze cairunze]

to rewrite inside quantifiers, probably we can try simp_rw [tsub_nonpos].

[Luigi Massacci]

I would bet money on conv working if simp_rw doesn’t cut it

[Luigi Massacci]

@loogle le_of_sub_nonneg

[loogle]

:search: le_of_sub_nonneg

[Luigi Massacci]

Oh and note that you need the tsub lebba @cairunze cairunze gave you, the other two are for additive groups, so the natural numbers sadly don’t qualify

[Giacomo Stevanato]

Going from A ≥ B to A - B ≥ 0 with natural numbers would be wrong. Note that - for natural numbers is defined to be saturating to 0, and A - B ≥ 0 is trivially true for any natural number. You have to go to the integers, but that complicates things.

[Luigi Massacci]

This is why tsub_nonpos rewrites to B - A <= 0

[Luigi Massacci]

But you are right to point out that maybe @rzeta0 you don’t really want to do this

[Ruben Van de Velde]

Note that's \le 0, not \ge 0