Step * of Lemma absval-non-neg

[x:ℤ]. (0 ≤ |x|)
BY
((UnivCD THENA Auto) THEN Decide 0 ∈ ℤ THEN Auto) }


Latex:


Latex:
\mforall{}[x:\mBbbZ{}].  (0  \mleq{}  |x|)


By


Latex:
((UnivCD  THENA  Auto)  THEN  Decide  x  =  0  THEN  Auto)




Home Index