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