---

Step * of Lemma qadd_functionality_wrt_qless_2

∀[a,b,c,d:ℚ].  (a + c < b + d) supposing (c < d and (a ≤ b))
BY
{ (Auto THEN Assert ⌜a + c < a + d⌝⋅) }

1
.....assertion..... 
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. d : ℚ
5. a ≤ b
6. c < d
⊢ a + c < a + d

2
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. d : ℚ
5. a ≤ b
6. c < d
7. a + c < a + d
⊢ a + c < b + d

---

Latex:

---

Latex:
\mforall{}[a,b,c,d:\mBbbQ{}].    (a  +  c  <  b  +  d)  supposing  (c  <  d  and  (a  \mleq{}  b))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}a  +  c  <  a  +  d\mkleeneclose{}\mcdot{})

---

Home Index