---

Step * of Lemma qadd_functionality_wrt_qless

∀[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  \mleq{}  d)  and  a  <  b)


By

---

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

---

Home Index