---

Step * of Lemma assert-ble

∀[n:ℤ]. ∀[m:ℕ].  (↑ble(n;m) ⇐⇒ n ≤ m)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``ble`` 0 THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[m:\mBbbN{}].    (\muparrow{}ble(n;m)  \mLeftarrow{}{}\mRightarrow{}  n  \mleq{}  m)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``ble``  0  THEN  Repeat  (AutoSplit))

---

Home Index