Step * of Lemma isOdd-2n+1

n:ℤ(isOdd((2 n) 1) tt)
BY
(Auto THEN RWO "eqtt_to_assert" THEN Auto THEN RWO  "assert-isOdd" THEN Auto) }


Latex:


Latex:
\mforall{}n:\mBbbZ{}.  (isOdd((2  *  n)  +  1)  \msim{}  tt)


By


Latex:
(Auto  THEN  RWO  "eqtt\_to\_assert"  0  THEN  Auto  THEN  RWO    "assert-isOdd"  0  THEN  Auto)




Home Index