---

Step * of Lemma max_tl_coeffs_wf

∀[n:ℕ+]. ∀[ineqs:{L:ℤ List| ||L|| = n ∈ ℤ}  List+].  (max_tl_coeffs(ineqs) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} )
BY
{ TACTIC:(Auto THEN RepeatFor 2 (DVar `ineqs')) }

1
1. n : ℕ+
2. 0 < ||[]||
⊢ max_tl_coeffs([]) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} 

2
1. n : ℕ+
2. u : {L:ℤ List| ||L|| = n ∈ ℤ} 
3. v : {L:ℤ List| ||L|| = n ∈ ℤ}  List
4. 0 < ||[u / v]||
⊢ max_tl_coeffs([u / v]) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[ineqs:\{L:\mBbbZ{}  List|  ||L||  =  n\}    List\msupplus{}].    (max\_tl\_coeffs(ineqs)  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\}\000C  )


By

---

Latex:
TACTIC:(Auto  THEN  RepeatFor  2  (DVar  `ineqs'))

---

Home Index