---

Step * of Lemma sqle_n_subtype_rel

∀[a,b:Base]. ∀[n:ℕ].  a ≤n b supposing a ≤n + 1 b
BY
{ Intros }

1
1. [a] : Base
2. [b] : Base
3. [n] : ℕ
4. [%] : a ≤n + 1 b
⊢ a ≤n b

---

Latex:

---

Latex:
\mforall{}[a,b:Base].  \mforall{}[n:\mBbbN{}].    a  \mleq{}n  b  supposing  a  \mleq{}n  +  1  b


By

---

Latex:
Intros

---

Home Index