---

Step * of Lemma test-q-norm-conv

∀[a,b,c:ℚ].  (((a + b) * (c + b)) = (((a * c) + (b * c)) + (b * b) + (a * b)) ∈ ℚ)
BY
{ xxx(Auto THEN RW (QNormC' ⌜a * c⌝) 0⋅ THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    (((a  +  b)  *  (c  +  b))  =  (((a  *  c)  +  (b  *  c))  +  (b  *  b)  +  (a  *  b)))


By

---

Latex:
xxx(Auto  THEN  RW  (QNormC'  \mkleeneopen{}a  *  c\mkleeneclose{})  0\mcdot{}  THEN  Auto)xxx

---

Home Index