---

Step * of Lemma test-rat-term-poly

No Annotations
∀[x,y:ℝ].  (r1/r1 + (y/x * x * x)) = (x * x * x/y + (x * x * x)) supposing (y < -(x * x * x)) ∧ x ≠ r0
BY
{ (Intros THEN Auto THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:\mBbbR{}].
    (r1/r1  +  (y/x  *  x  *  x))  =  (x  *  x  *  x/y  +  (x  *  x  *  x))  supposing  (y  <  -(x  *  x  *  x))  \mwedge{}  x  \mneq{}  r0


By

---

Latex:
(Intros  THEN  Auto  THEN  EAuto  1)

---

Home Index