Step
*
of Lemma
rminus-reverses-rleq
∀[x,y:ℝ]. -(y) ≤ -(x) supposing x ≤ y
BY
{ (Unfold `rleq` 0 THEN Auto) }
1
1. x : ℝ
2. y : ℝ
3. rnonneg(y - x)
⊢ rnonneg(-(x) - -(y))
Latex:
Latex:
\mforall{}[x,y:\mBbbR{}]. -(y) \mleq{} -(x) supposing x \mleq{} y
By
Latex:
(Unfold `rleq` 0 THEN Auto)
Home
Index