Step
*
of Lemma
absval-squeeze
∀[a,b,c,d:ℤ]. |b - c| ≤ (d - a) supposing ((a ≤ b) ∧ (b ≤ d)) ∧ (a ≤ c) ∧ (c ≤ d)
BY
{ (Auto THEN RWO "absval_unfold" 0 THEN Repeat (AutoSplit) THEN Auto) }
Latex:
Latex:
\mforall{}[a,b,c,d:\mBbbZ{}]. |b - c| \mleq{} (d - a) supposing ((a \mleq{} b) \mwedge{} (b \mleq{} d)) \mwedge{} (a \mleq{} c) \mwedge{} (c \mleq{} d)
By
Latex:
(Auto THEN RWO "absval\_unfold" 0 THEN Repeat (AutoSplit) THEN Auto)
Home
Index