---

Step * of Lemma add-monotonic

∀a,b,c,d:ℤ.  (a < b ⇒ ((c = d ∈ ℤ) ∨ c < d) ⇒ a + c < b + d)
BY
{ (Auto THEN D 0 THEN Auto THEN UnfoldTopAb 0 THEN Assert ⌜if (a + c) < (b + c)  then True  else False⌝⋅) }

1
.....assertion..... 
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. d : ℤ
5. a < b
6. (c = d ∈ ℤ) ∨ c < d
⊢ if (a + c) < (b + c)  then True  else False

2
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. d : ℤ
5. a < b
6. (c = d ∈ ℤ) ∨ c < d
7. if (a + c) < (b + c)  then True  else False
⊢ if (a + c) < (b + d)  then True  else False

---

Latex:

---

Latex:
\mforall{}a,b,c,d:\mBbbZ{}.    (a  <  b  {}\mRightarrow{}  ((c  =  d)  \mvee{}  c  <  d)  {}\mRightarrow{}  a  +  c  <  b  +  d)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  UnfoldTopAb  0
  THEN  Assert  \mkleeneopen{}if  (a  +  c)  <  (b  +  c)    then  True    else  False\mkleeneclose{}\mcdot{})

---

Home Index