Proving inequalities over the reals involving division

Stream: general

[Brendan Seamas Murphy]

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]

Have you tried nlinarith? That should be enough here.

[Brendan Seamas Murphy]

Nope, it fails

[Brendan Seamas Murphy]

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]

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]

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

[Yaël Dillies]

I don't see it.

[Brendan Seamas Murphy]

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]

There is a 1 / c in front.

[Brendan Seamas Murphy]

oh lol you're completely right

[Brendan Seamas Murphy]

thanks, I'll try that