Step
*
of Lemma
nat-mono
mono(ℕ)
BY
{ (Unfold `nat` 0 THEN BLemma `set-mono` THEN Auto THEN BLemma `int-mono`) }
Latex:
Latex:
mono(\mBbbN{})
By
Latex:
(Unfold  `nat`  0  THEN  BLemma  `set-mono`  THEN  Auto  THEN  BLemma  `int-mono`)
Home
Index