Step * 1 1 1 1 1 of Lemma div_bounds_2


1. n : ℕ+
2. v : ℤ
3. v1 : ℤ
⊢ (-n) + v1 < v ⇒ (0 ≤ ((-n) + v1)) ⇒ 0 < v
BY
{ Auto }


Latex:


Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  v  :  \mBbbZ{}
3.  v1  :  \mBbbZ{}
\mvdash{}  (-n)  +  v1  <  v  {}\mRightarrow{}  (0  \mleq{}  ((-n)  +  v1))  {}\mRightarrow{}  0  <  v


By


Latex:
Auto




Home Index