a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ a * d ≤ c * b
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a /. b ≤ c /. d ↔ a * d ≤ c * b
rw [Rat.le_iff_Nonneg]
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ a * d ≤ c * b
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ a * d ≤ c * b
show Rat.Nonneg _ ↔ _
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ 0 ≤ c * b - a * d
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ a * d ≤ c * b
rw [← sub_nonneg]
no goals
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ Rat.Nonneg (c /. d - a /. b) ↔ 0 ≤ c * b - a * d
simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, mul_pos d0 b0]