Step
*
of Lemma
qinv_assoc_q
No Annotations
∀[a,b:ℚ].  (((a + -(a) + b) = b ∈ ℚ) ∧ ((-(a) + a + b) = b ∈ ℚ))
BY
{ (ProveSpecializedLemmaWReduce grp_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  grp\_inv\_assoc)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}
Home
Index