---

Step * of Lemma qle-normalize

∀[a,b:ℚ].  uiff(a ≤ b;0 ≤ (b - a))
BY
{ Auto }

1
1. a : ℚ
2. b : ℚ
3. a ≤ b
⊢ 0 ≤ (b - a)

2
1. a : ℚ
2. b : ℚ
3. 0 ≤ (b - a)
⊢ a ≤ b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    uiff(a  \mleq{}  b;0  \mleq{}  (b  -  a))


By

---

Latex:
Auto

---

Home Index