---

Step * of Lemma rless-witness-property

∀[x,y:ℝ]. ∀[p:x < y].  ((x ≤ (y - (r1/r(rless-witness(x;y;p))))) ∧ ((x + (r1/r(rless-witness(x;y;p)))) ≤ y))
BY
{ (BasicUniformUnivCD Auto
   THEN (InstLemma `rless-witness_wf` [⌜x⌝;⌜y⌝;⌜p⌝]⋅ THENA Auto)
   THEN Unhide
   THEN Try (Complete ((Auto THEN GenConcl ⌜rless-witness(x;y;p) = k ∈ ℕ+⌝⋅ THEN Auto)))
   THEN (GenConcl ⌜rless-witness(x;y;p) = k ∈ ℕ+⌝⋅ THENA Auto)
   THEN (MoveToConcl (-1)
         THEN Unfold `rless-witness` 0
         THEN (GenConclAtAddr [1;2;1] ⋅ THENA Auto)
         THEN D (-2)
         THEN Reduce 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].  \mforall{}[p:x  <  y].
    ((x  \mleq{}  (y  -  (r1/r(rless-witness(x;y;p)))))  \mwedge{}  ((x  +  (r1/r(rless-witness(x;y;p))))  \mleq{}  y))


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  (InstLemma  `rless-witness\_wf`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unhide
  THEN  Try  (Complete  ((Auto  THEN  GenConcl  \mkleeneopen{}rless-witness(x;y;p)  =  k\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  (GenConcl  \mkleeneopen{}rless-witness(x;y;p)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl  (-1)
              THEN  Unfold  `rless-witness`  0
              THEN  (GenConclAtAddr  [1;2;1]  \mcdot{}  THENA  Auto)
              THEN  D  (-2)
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index