Step
*
of Lemma
less_than_anti-reflexive
∀[x:ℤ]. (¬x < x)
BY
{ (InstLemma `less_than_irreflexivity` [] THEN Fold `not` (-1) THEN Trivial) }
Latex:
Latex:
\mforall{}[x:\mBbbZ{}].  (\mneg{}x  <  x)
By
Latex:
(InstLemma  `less\_than\_irreflexivity`  []  THEN  Fold  `not`  (-1)  THEN  Trivial)
Home
Index