## Stream: general

### Topic: Proving inequalities over the reals involving division

#### Brendan Seamas Murphy (Aug 21 2022 at 22:23):

Is there a tactic that will automatically solve the following goal? image.png
linarith doesn't work because, well, the inequality isn't remotely linear. I'm hoping I don't have to do this manually...

#### Yaël Dillies (Aug 21 2022 at 22:35):

Have you tried nlinarith? That should be enough here.

Nope, it fails

#### Brendan Seamas Murphy (Aug 21 2022 at 22:39):

I realized the manual proof wouldn't be as bad as I feared (I had structured things earlier so that this would happen and forgotten about it) but I'd still like a magic tactic

#### Alex J. Best (Aug 21 2022 at 22:42):

If you clear the denominators it becomes linear right? So if you first show c is nonzero then use tactic#field_simp (or manually clear denominators) you might get to something linarith will work on

#### Brendan Seamas Murphy (Aug 21 2022 at 22:45):

won't you have a c^2 term if you just clear denominators?

I don't see it.

#### Brendan Seamas Murphy (Aug 21 2022 at 22:47):

the last term in the product on the right hand side is a 1 - c, and clearing denominators will multiply this by c

#### Yaël Dillies (Aug 21 2022 at 22:47):

There is a 1 / c in front.

#### Brendan Seamas Murphy (Aug 21 2022 at 22:47):

oh lol you're completely right

#### Brendan Seamas Murphy (Aug 21 2022 at 22:47):

thanks, I'll try that

Last updated: Dec 20 2023 at 11:08 UTC