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