---

Step * 1 of Lemma test-arith-length-additions


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

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  a  :  T@i
3.  b  :  T  List@i
4.  i  :  \mBbbZ{}@i
5.  i  <  ||[a  /  b]||@i
\mvdash{}  i  <  ||b||  +  1


By

---

Latex:
Auto

---

Home Index