---

Step * of Lemma add-nonneg

∀x,y:ℤ.  (0 ≤ (x + y)) supposing ((0 ≤ x) and (0 ≤ y))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (RWO "le-iff-less-or-equal" 0 THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN ((Decide ⌜0 = y ∈ ℤ⌝⋅ THENA Auto) THEN Try ((RevHypSubst' (-1) 0 THENA Auto)))
   THEN (Decide ⌜0 = x ∈ ℤ⌝⋅ THENA Auto)
   THEN Try ((RevHypSubst' (-1) 0 THENA Auto))
   THEN Try (((OrRight THENA Auto) THEN Reduce 0 THEN EqCD))
   THEN (OrLeft THENA Auto)
   THEN (RW IntNormC 0 THENA Auto)
   THEN ∀h:hyp. DOr h⋅ 
   THEN Try (Trivial)) }

1
1. x : ℤ@i
2. y : ℤ@i
3. 0 < y
4. 0 < x
5. ¬(0 = y ∈ ℤ)
6. ¬(0 = x ∈ ℤ)
⊢ 0 < x + y

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    (0  \mleq{}  (x  +  y))  supposing  ((0  \mleq{}  x)  and  (0  \mleq{}  y))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (RWO  "le-iff-less-or-equal"  0  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ((Decide  \mkleeneopen{}0  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Try  ((RevHypSubst'  (-1)  0  THENA  Auto)))
  THEN  (Decide  \mkleeneopen{}0  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((RevHypSubst'  (-1)  0  THENA  Auto))
  THEN  Try  (((OrRight  THENA  Auto)  THEN  Reduce  0  THEN  EqCD))
  THEN  (OrLeft  THENA  Auto)
  THEN  (RW  IntNormC  0  THENA  Auto)
  THEN  \mforall{}h:hyp.  DOr  h\mcdot{} 
  THEN  Try  (Trivial))

---

Home Index