---

Step * of Lemma rsqrt0

rsqrt(r0) = r0
BY
{ ((BLemma `req_inversion` THENA Auto) THEN BLemma `rsqrt-unique` THEN Auto) }

---

Latex:

---

Latex:
rsqrt(r0)  =  r0


By

---

Latex:
((BLemma  `req\_inversion`  THENA  Auto)  THEN  BLemma  `rsqrt-unique`  THEN  Auto)

---

Home Index