---

Step * of Lemma radd-rmin

∀[x,y,z:ℝ].  ((x + rmin(y;z)) = rmin(x + y;x + z))
BY
{ (Auto
   THEN (BLemma `req-iff-bdd-diff` THENA Auto)
   THEN (RWO "radd-bdd-diff" 0 THENA (Try (Complete (Auto)) THEN RepUR ``rmin`` 0 THEN Auto))
   THEN RepUR ``rmin`` 0
   THEN BLemma `trivial-bdd-diff`
   THEN Auto
   THEN Reduce 0) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. n : ℕ+
⊢ ((x n) + imin(y n;z n)) = imin((x n) + (y n);(x n) + (z n)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    ((x  +  rmin(y;z))  =  rmin(x  +  y;x  +  z))


By

---

Latex:
(Auto
  THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto)
  THEN  (RWO  "radd-bdd-diff"  0  THENA  (Try  (Complete  (Auto))  THEN  RepUR  ``rmin``  0  THEN  Auto))
  THEN  RepUR  ``rmin``  0
  THEN  BLemma  `trivial-bdd-diff`
  THEN  Auto
  THEN  Reduce  0)

---

Home Index