---

Step * of Lemma add_functionality_wrt_lt

∀[i1,i2,j1,j2:ℤ].  (i1 + i2 < j1 + j2) supposing ((i2 ≤ j2) and i1 < j1)
BY
{ ((UnivCD THENA Auto) THEN BLemma `add-monotonic` THEN Auto) }

1
1. i1 : ℤ
2. i2 : ℤ
3. j1 : ℤ
4. j2 : ℤ
5. i1 < j1
6. i2 ≤ j2
⊢ (i2 = j2 ∈ ℤ) ∨ i2 < j2

---

Latex:

---

Latex:
\mforall{}[i1,i2,j1,j2:\mBbbZ{}].    (i1  +  i2  <  j1  +  j2)  supposing  ((i2  \mleq{}  j2)  and  i1  <  j1)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  BLemma  `add-monotonic`  THEN  Auto)

---

Home Index