---

Step * 1 of Lemma int_is_mono


1. x : ℤ
2. y : Base
3. x ≤ y
4. (y)↓
⊢ y ≤ x
BY
{ ((Assert ⌜x + 0 ≤ y + 0⌝⋅ THENA Auto) THEN FLemma `has-value-monotonic` [-1] THEN Auto THEN HasValueD (-1)) }

1
1. x : ℤ
2. y : Base
3. x ≤ y
4. (y)↓
5. x + 0 ≤ y + 0
6. (y + 0)↓
7. y ∈ ℤ
8. 0 ∈ ℤ
⊢ y ≤ x

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  Base
3.  x  \mleq{}  y
4.  (y)\mdownarrow{}
\mvdash{}  y  \mleq{}  x


By

---

Latex:
((Assert  \mkleeneopen{}x  +  0  \mleq{}  y  +  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  FLemma  `has-value-monotonic`  [-1]
  THEN  Auto
  THEN  HasValueD  (-1))

---

Home Index