---

Step * 1 of Lemma is-above-int


1. n : ℤ
2. z : Base
3. y : Base
4. y = n ∈ ℤ
5. y ≤ z
⊢ z = n ∈ ℤ
BY
{ (InstLemma `int_is_mono` []⋅ THEN (Assert ⌜n ~ z⌝⋅ THENM (RWO "-1<" 0 THEN Auto)) THEN SqequalSqle THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  z  :  Base
3.  y  :  Base
4.  y  =  n
5.  y  \mleq{}  z
\mvdash{}  z  =  n


By

---

Latex:
(InstLemma  `int\_is\_mono`  []\mcdot{}
  THEN  (Assert  \mkleeneopen{}n  \msim{}  z\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1<"  0  THEN  Auto))
  THEN  SqequalSqle
  THEN  Auto)\mcdot{}

---

Home Index