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