---

Step * of Lemma test-arith-length-additions

∀T:Type. ∀a:T. ∀b:T List. ∀i:ℤ.  (i < ||[a / b]|| ⇒ i < ||b|| + 1)
BY
{ (UnivCD THENA Auto) }

1
1. T : Type@i'
2. a : T@i
3. b : T List@i
4. i : ℤ@i
5. i < ||[a / b]||@i
⊢ i < ||b|| + 1

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}a:T.  \mforall{}b:T  List.  \mforall{}i:\mBbbZ{}.    (i  <  ||[a  /  b]||  {}\mRightarrow{}  i  <  ||b||  +  1)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index