---

Step * of Lemma sqlen_sqequaln

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

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

---

Latex:

---

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


By

---

Latex:
Intros

---

Home Index