---

Step * of Lemma qadd_functionality_wrt_qle

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


By

---

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

---

Home Index