---

Step * of Lemma qinv_inv_q

No Annotations
∀[a:ℚ]. (-(-(a)) = a ∈ ℚ)
BY
{ (ProveSpecializedLemmaWReduce grp_inv_inv) 0 [⌜parm{i}⌝;⌜<ℚ+>⌝]⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  (-(-(a))  =  a)


By

---

Latex:
(ProveSpecializedLemmaWReduce  grp\_inv\_inv)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}

---

Home Index