# Zulip Chat Archive

## Stream: new members

### Topic: Lean's way of simple term transformations

#### André Beyer (Jan 21 2021 at 17:00):

Hi!

I'm often struggling with transforming terms from one to another. Here's an example:

```
h : 0 ≤ (n - 1) ^ 2
⊢ 2 ≤ n + 1 / n
```

This is easy on paper:

$0 \le (n - 1)^2 \iff 0 \le n^2 - 2n + 1 \iff 2n \le n^2 + 1 \iff 2 \le n + \frac{1}{n}$

I don't know how to best archive this using Lean - what are the best practices in such cases? Any suggestions? Thanks in advance!

#### Bryan Gin-ge Chen (Jan 21 2021 at 17:04):

I suppose `n`

is a natural number coerced to a rational number? Note that you'll need an additional hypothesis of `n \ne 0`

since `1/0`

is defined to be `0`

in mathlib.

#### Lars Ericson (Jan 21 2021 at 17:08):

Something like this plus what Bryan just said:

```
import tactic
theorem ineq_on_n (n: ℕ) : 0 ≤ (n-1)^2 ↔ 2*n ≤ n^2+1 :=
begin
split,
{
intro h,
refine eq.le _,
sorry,
},
{
intro h,
exact zero_le ((n - 1) ^ 2),
}
end
```

#### Johan Commelin (Jan 21 2021 at 17:44):

@André Beyer Please state problems in the form of

```
import whatever.you.need
example (n : nat?rat?real?) : etc :=
sorry
```

See also #mwe <- this is a link

#### Mario Carneiro (Jan 21 2021 at 17:53):

Here's a proof along those general lines:

```
import data.real.basic
example (n : ℝ) (h : n > 0) : 2 ≤ n + 1 / n :=
begin
refine le_of_mul_le_mul_left _ h,
simp [mul_add, ne_of_gt h],
rw ← sub_nonneg,
convert pow_two_nonneg (n - 1),
ring,
end
```

#### Mario Carneiro (Jan 21 2021 at 17:54):

the hard part is dealing with the division, as others said

#### Mario Carneiro (Jan 21 2021 at 17:54):

for the most part you can just clear denominators, make it a polynomial equation, and let `ring`

take care of the rest

#### Bryan Gin-ge Chen (Jan 21 2021 at 17:56):

I was just writing up a very similar proof which uses `field_simp`

instead of the explicit lemma `le_of_mul_le_mul_left`

:

```
import tactic
import tactic.field_simp
example {n : ℚ} (h : 0 < n) : 2 ≤ n + 1 / n :=
begin
have H : n*n + 1 - 2*n = (n - 1) * (n - 1) := by ring,
field_simp [ne_of_gt h],
rw [le_div_iff h, ← sub_nonneg, H],
exact mul_self_nonneg _,
end
```

#### Mario Carneiro (Jan 21 2021 at 17:58):

Ah, so that's how you are supposed to use `field_simp`

here. You can also put the `ring`

at the end like this:

```
example (n : ℝ) (h : n > 0) : 2 ≤ n + 1 / n :=
begin
field_simp [ne_of_gt h],
rw [le_div_iff h, ← sub_nonneg],
convert pow_two_nonneg (n - 1),
ring,
end
```

#### André Beyer (Jan 21 2021 at 19:59):

Looks good, thank you!

Last updated: May 08 2021 at 18:17 UTC