Step
*
2
of Lemma
rleq-int-fractions3
1. a : ℤ
2. b : ℤ
3. d : ℕ+
4. b ≤ (a * d)
⊢ (r(b)/r(d)) ≤ r(a)
BY
{ (nRMul ⌜r(d)⌝ 0⋅ THEN Auto) }
Latex:
Latex:
1. a : \mBbbZ{}
2. b : \mBbbZ{}
3. d : \mBbbN{}\msupplus{}
4. b \mleq{} (a * d)
\mvdash{} (r(b)/r(d)) \mleq{} r(a)
By
Latex:
(nRMul \mkleeneopen{}r(d)\mkleeneclose{} 0\mcdot{} THEN Auto)
Home
Index