---

Step * of Lemma qadd_inv_assoc_q

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

---

Latex:

---

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


By

---

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

---

Home Index