---

Step * of Lemma qinv_thru_op_q

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

---

Latex:

---

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


By

---

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

---

Home Index