---

Step * of Lemma int_is_mono

∀[x:ℤ]. ∀[y:Base].  y ≤ x supposing x ≤ y
BY
{ SqReasoning }

1
1. x : ℤ
2. y : Base
3. x ≤ y
4. (y)↓
⊢ y ≤ x

2
1. x : ℤ
2. y : Base
3. x ≤ y
4. is-exception(y)
⊢ y ≤ x

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[y:Base].    y  \mleq{}  x  supposing  x  \mleq{}  y


By

---

Latex:
SqReasoning

---

Home Index