## Stream: new members

### Topic: How to prove (-2) * m * m + m ^ 2 ≤ (-2) * m * m' + m' ^ 2

#### Marko Grdinić (Oct 16 2019 at 14:09):

More specifically example (m m' : rat) : (-2) * m * m + m ^ 2 ≤ (-2) * m * m' + m' ^ 2. The way to solve this is to add m ^ 2 on both sides which after simplifying should result in 0 <= (m - m')^2. The issue I am having is that for some reason ring is acting crazy and not simplifying anything. Sure I could pry this problem into shape using step by step tactics, but I am wondering if there is an elegant approach to this.

#### Mario Carneiro (Oct 16 2019 at 14:12):

ring is not a simplifier

#### Mario Carneiro (Oct 16 2019 at 14:12):

it's supposed to kill the goal

#### Mario Carneiro (Oct 16 2019 at 14:12):

it sometimes simplifies as a side effect but you shouldn't rely on it

#### Mario Carneiro (Oct 16 2019 at 14:13):

Also, those two expressions are already "simplified" from the POV of ring

#### Mario Carneiro (Oct 16 2019 at 14:22):

example (m m' : rat) : (-2) * m * m + m ^ 2 ≤ (-2) * m * m' + m' ^ 2 :=
@le_of_add_le_add_right _ _ _ (m^2) _ \$
by convert (pow_two_nonneg (m - m')); ring


#### Marko Grdinić (Oct 16 2019 at 14:50):

Here is what I came up with. I definitely like your solution better.

example (m m' : rat) : (-2) * m * m + m ^ 2 ≤ (-2) * m * m' + m' ^ 2 :=
by {
simp,
rw [mul_assoc, ← pow_two, ← add_assoc],
rw add_comm (m' ^ 2) (2 * m ^ 2),
rw two_mul,
rw add_comm (m' ^ 2) (-(2 * m * m')),
have : (m - m') ^ 2 = m ^ 2 + ((- (2 * m * m')) + m' ^ 2), by ring,
rw ← this,
apply pow_two_nonneg
}


Thanks.

#### Kenny Lau (Oct 16 2019 at 23:39):

import data.rat tactic.ring

example (m m' : rat) : (-2) * m * m + m ^ 2 ≤ (-2) * m * m' + m' ^ 2 :=
calc  (-2) * m * m + m ^ 2
≤ (-2) * m * m + m ^ 2 + (m-m')^2 : le_add_of_nonneg_right (pow_two_nonneg _)
... = (-2) * m * m' + m' ^ 2          : by ring


Last updated: May 18 2021 at 17:44 UTC