Revision history [back]

I have an inequality in multiple variables and want to show that it is true given that the variables satisfy some conditions (also formulated as inequalities).

I come from Mathematica, where I can write Reduce[Implies[0<x<1, x>x^2], Reals] and get true as the answer. Is Sage (maybe with some optional package) able to verify these kinds of implications?

This is a simplified implication I want to show: $0 < f \leq 1$ and $z \geq \frac{1}{\sqrt{1+0.8f}}$, implies $$\left((z+f)^2-f^2-1\right)^2+\left((z-1+2f)^2-4f^2\right) > 0$$

So far I tried qepcad but the following code just ran forever:

var('z, f'); qf = qepcad_formula;
qepcad( qf.implies(qf.and_(f>0, f<=1, z>=1/(sqrt(1+4*f/5))), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0) )

Are there better ways to formulate my statement using qepcad, are there better packages available or is Sage not able to help me here?

Note that I don't need help for the given example, as I proved this already. However I have similar more complicated implications of the same form which I need to check using some other CAS than Mathematica. Can Coq do this?

I have an inequality in multiple variables and want to show that it is true given that the variables satisfy some conditions (also formulated as inequalities).

I come from Mathematica, where I can write Reduce[Implies[0<x<1, x>x^2], Reals] and get true as the answer. Is Sage (maybe with some optional package) able to verify these kinds of implications?

This is a simplified implication I want to show: $0 < f \leq 1$ and $z \geq \frac{1}{\sqrt{1+0.8f}}$, implies $$\left((z+f)^2-f^2-1\right)^2+\left((z-1+2f)^2-4f^2\right) > 0$$

So far I tried qepcad but the following code just ran forever:

var('z, f'); qf = qepcad_formula;
qepcad( qf.implies(qf.and_(f>0, f<=1, z>=1/(sqrt(1+4*f/5))), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0) )

Are there better ways to formulate my statement using qepcad, are there better packages available or is Sage not able to help me here?

Note that I don't need help for the given example, as I proved this already. However I have similar more complicated implications of the same form which I need to check using some other CAS than Mathematica. Can Coq do this?