---

Step * of Lemma sqequaln_sqlen

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

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

---

Latex:

---

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


By

---

Latex:
Intros

---

Home Index