Step * of Lemma div_minus_one

No Annotations
[x:ℤ]. (x ÷ -1 -x)
BY
(Auto THEN BLemma `div_unique3` THEN Auto THEN With ⌜0⌝  THEN Auto) }


Latex:


Latex:
No  Annotations
\mforall{}[x:\mBbbZ{}].  (x  \mdiv{}  -1  \msim{}  -x)


By


Latex:
(Auto  THEN  BLemma  `div\_unique3`  THEN  Auto  THEN  D  0  With  \mkleeneopen{}0\mkleeneclose{}    THEN  Auto)




Home Index