---

Step * 1 1 1 1 1 1 of Lemma egyptian-fraction

.....equality..... 
1. a : ℕ
2. a = 0 ∈ ℤ
3. b : ℕ
4. 0 < b
⊢ ||[]|| ~ 0
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  a  :  \mBbbN{}
2.  a  =  0
3.  b  :  \mBbbN{}
4.  0  <  b
\mvdash{}  ||[]||  \msim{}  0


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index