---

Step * of Lemma le_weakening

∀a,b:ℤ.  a ≤ b supposing a = b ∈ ℤ
BY
{ ((UnivCD THENA Auto) THEN (RWO "le-iff-less-or-equal" 0 THENA Auto)) }

1
1. a : ℤ@i
2. b : ℤ@i
3. a = b ∈ ℤ
⊢ a < b ∨ (a = b ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    a  \mleq{}  b  supposing  a  =  b


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "le-iff-less-or-equal"  0  THENA  Auto))

---

Home Index