Step * 1 1 1 1 1 of Lemma div_bounds_2


1. : ℕ+
2. : ℤ
3. v1 : ℤ
⊢ (-n) v1 <  (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