---

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

∀L:ℤ List. ∀[x:ℕ]. (imax-list([x / L]) ∈ ℕ)
BY
{ (Auto THEN MemTypeCD THEN Auto THEN BLemma `imax-list-ub` THEN Auto) }

1
1. L : ℤ List
2. x : ℕ
⊢ (∃b∈[x / L]. 0 ≤ b)

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List.  \mforall{}[x:\mBbbN{}].  (imax-list([x  /  L])  \mmember{}  \mBbbN{})


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto  THEN  BLemma  `imax-list-ub`  THEN  Auto)

---

Home Index