---

Step * of Lemma frs-increasing-non-dec

∀[p:ℝ List]. (frs-increasing(p) ⇒ frs-non-dec(p))
BY
{ (Auto
   THEN All (Unfolds ``frs-non-dec frs-increasing``)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto
   THEN (Decide ⌜i = j ∈ ℤ⌝⋅ THENA Auto)
   THEN Try ((HypSubst' (-1) 0 THEN RelRST THEN Auto))
   THEN (InstHyp [⌜i⌝;⌜j⌝] 2⋅ THEN Auto)
   THEN RelRST
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbR{}  List].  (frs-increasing(p)  {}\mRightarrow{}  frs-non-dec(p))


By

---

Latex:
(Auto
  THEN  All  (Unfolds  ``frs-non-dec  frs-increasing``)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  (Decide  \mkleeneopen{}i  =  j\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((HypSubst'  (-1)  0  THEN  RelRST  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  2\mcdot{}  THEN  Auto)
  THEN  RelRST
  THEN  Auto)

---

Home Index