Recenty in sci.math.symbolic there was a question if

(1)

and

(2)

implies

(3)

or

(4)

This can be proved by an elementary argument. Below w show purely mechanical way based on cylindrical algebraic decomposition (CAD).

(1) -> rC := RealClosure(Fraction(Integer))

(5)

pR := POLY(rC)

(6)

-- Replace inequalies by differences of sides
lp := [b^2 - (a - c)^2, a^2 - b^2, c^2 - (a + b)^2, c^2 - (a - b)^2]

(7)

-- Do CAD
cd := cylindricalDecomposition(lp::List(pR)
                              )$CylindricalAlgebraicDecompositionPackage(rC)

(8)

-- If implication is false, then there is opposite strict ineqality
-- in the last two inequalities.  Hence, there is counterexample where
-- all inequalities are strict.  Consequently, it is enough to look
-- only at cells of full dimension.
cd3 := [ce for ce in cd | dimension(ce) = 3];

sp3 := [samplePoint(ce) for ce in cd3]::List(List(Fraction(Integer)))

(9)

vll := [map(p +-> eval(p, [a, b, c], pp), lp) for pp in sp3];

vlq := vll::List(List(Fraction(Integer)))

(10)

good := true

(11)

-- Loop to check validity of formula at each sample point
for vl in vlq repeat
    if vl(1) > 0 and vl(2) > 0 and vl(3) < 0 and vl(4) < 0 then
        good := false

print good

   true

Let us explain this a bit more. CAD for list of polynomials l produces collection of cells such that any boolean formula in equations and inequalites of polynomials in l produces constant value on each cells. And cells cover the whole space. So, to check validity of Boolean formula it is enough to check its validity on each cell. Since value of the formula is constant in the cell it is enough to compute value at single point given by samplePoint. Above we took advantage of another property: closure of sum of cells of full dimension gives the whole space. Since sets on which assumptions and conclusion of our formula hold are closed we can gain a little extra efficiency and ignore cells of lower dimension.