# Zulip Chat Archive

## Stream: new members

### Topic: IFF Question

#### Dev-Indra (Mar 19 2020 at 16:07):

Here is the `iff`

lemma I am trying to prove:

lemma another_helper (u v : ℕ) : v ≤ u ↔ v*v ≤ v*u := begin split, induction v with d hd, rw mul_zero, rw zero_mul, simp, rw succ_eq_add_one, rw mul_add, rw mul_one, rw mul_comm, rw mul_add, rw mul_one, rw add_mul, rw one_mul, end

I am trying to prove the first goal with induction, but I am stuck after the last line. Can anyone help, or suggest a better way to prove this?

#### Kevin Buzzard (Mar 19 2020 at 16:48):

You should use `{}`

brackets to ensure that you only have one goal at all times. Your question is hard for me to understand because your code doesn't compile and I'm not entirely sure which rewrites are supposed to apply to which goals.

#### Shing Tak Lam (Mar 19 2020 at 16:48):

There is a lemma in `mathlib`

called `mul_le_mul_left`

, which you can use by importing `data.nat.basic`

. To solve your inductive case here, you can just use

intro h, apply nat.mul_le_mul_left (succ d) h,

instead of the bunch of `rw`

s. Which will close the goal.

Also you don't need induction here, since you don't need the induction hypotheses.

As `mul_le_mul_left`

is already an iff statement, you can pretty much just use it to solve your goal without needing to `split`

it.

A complete proof just using `mul_le_mul_left`

as an `iff`

statement is like this:

lemma another_helper (u v : ℕ) : v ≤ u ↔ v*v ≤ v*u := begin cases v, { split, { intro h, simp, }, intro, exact zero_le u, }, { symmetry, apply mul_le_mul_left, simp, } end

#### Kevin Buzzard (Mar 19 2020 at 16:49):

@Dev-Indra: note the brackets @Shing Tak Lam used!

#### Shing Tak Lam (Mar 19 2020 at 16:56):

I've golfed it slightly :) Apparently `norm_num`

is a lot more powerful than I thought.

lemma another_helper (u v : ℕ) : v ≤ u ↔ v*v ≤ v*u := begin cases v, { norm_num }, norm_num end

Curiously, just `norm_num`

by itself doesn't work, but using `cases`

then `norm_num`

does.

#### Dev-Indra (Mar 19 2020 at 16:58):

Thanks. @Kevin Buzzard I will take note of the use of {}

Last updated: May 14 2021 at 04:22 UTC