Step * of Lemma qinv_assoc_q

No Annotations
[a,b:ℚ].  (((a -(a) b) b ∈ ℚ) ∧ ((-(a) b) b ∈ ℚ))
BY
(ProveSpecializedLemmaWReduce grp_inv_assoc) [⌜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