abv a - abv b ≤ abv (a + b)

Stream: Is there code for X?

[Geoffrey Irving]

There's absolute_value.le_sub. Is there a reason there isn't absolute_value.le_add?

[Yakov Pechersky]

Do you mean docs#absolute_value.add_le?

[Geoffrey Irving]

No, I want abv a - abv b ≤ abv (a + b).

[Adam Topaz]

Just rearrange the triangle inequality?

[Geoffrey Irving]

Yes, I know how to prove it, but I need it as a lemma to do apply_rules. Should I send a PR, or does it exist somewhere that I didn’t notice?

[Adam Topaz]

Oh I see...

[Adam Topaz]

Is it possible to pass a term to apply_rules? I don't remember. If so, just pass in the term for the proof using g the usual triangle inequality

[Heather Macbeth]

My intuition with inequality proofs (on paper as well as in Lean) is to arrange them in such a way that there is no negation. I suspect metaprogramming will also be more convenient if you keep to this rule. So, can you phrase your intended proofs to involve

abv ((a + b) - b) ≤ abv (a + b) + abv b

instead?

[Geoffrey Irving]

Why does that logic not apply to le_sub?

[Heather Macbeth]

Well, in fact, I would probably also reorganize to avoid le_sub :)