---

Step * of Lemma add_functionality_wrt_le

∀[i1,i2,j1,j2:ℤ].  ((i1 + i2) ≤ (j1 + j2)) supposing ((i2 ≤ j2) and (i1 ≤ j1))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN (All (RWO "le-iff-less-or-equal") THENA Auto)
          THEN SplitOrHyps
          THEN Try (((OrRight THENM (EqCD THEN Trivial)) THENA Auto))
          THEN (OrLeft THENA Auto)
          THEN Try (TACTIC:(BLemma `add-monotonic` THEN Complete (Auto)))) }

1
1. i1 : ℤ
2. i2 : ℤ
3. j1 : ℤ
4. j2 : ℤ
5. i1 = j1 ∈ ℤ
6. i2 < j2
⊢ i1 + i2 < j1 + j2

---

Latex:

---

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


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  (All  (RWO  "le-iff-less-or-equal")  THENA  Auto)
                THEN  SplitOrHyps
                THEN  Try  (((OrRight  THENM  (EqCD  THEN  Trivial))  THENA  Auto))
                THEN  (OrLeft  THENA  Auto)
                THEN  Try  (TACTIC:(BLemma  `add-monotonic`  THEN  Complete  (Auto))))

---

Home Index