COF_T35
Premises:
(forall ?X (=> (not (= ?X 0)) (= (* ?X (recip ?X)) 1))) (not (= 0 1)) (forall ?X (or (=< 0 ?X) (=< 0 (neg ?X)))) (forall ?X (=> (not (= ?X 0)) (or (not (=< 0 ?X)) (not (=< 0 (neg ?X)))))) (forall (?X ?Y) (=> (and (=< 0 ?X) (=< 0 ?Y)) (=< 0 (* ?X ?Y)))) (forall (?X ?Y) (= (* ?X (neg ?Y)) (neg (* ?X ?Y)))) (=< 0 1)
Conclusion:
(forall ?Z (=> (and (=< 0 ?Z) (not (= ?Z 0))) (=< 0 (recip ?Z))))