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