---

Step * 1 of Lemma imax-list-cons-is-nat


1. L : ℤ List
2. x : ℕ
⊢ (∃b∈[x / L]. 0 ≤ b)
BY
{ (With ⌜0⌝ (D 0)⋅ THEN Auto THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  x  :  \mBbbN{}
\mvdash{}  (\mexists{}b\mmember{}[x  /  L].  0  \mleq{}  b)


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index