a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
have d₁0 : 0 < (d₁ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₁)
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
have d₂0 : 0 < (d₂ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₂)
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * n₂
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ Rat.Nonneg (n₁ /. ↑d₁) → Rat.Nonneg (n₂ /. ↑d₂) → Rat.Nonneg (n₁ /. ↑d₁ * (n₂ /. ↑d₂))
rw [mul_def' d₁0.ne.symm d₂0.ne.symm, divInt_nonneg _ d₁0, divInt_nonneg _ d₂0,
  divInt_nonneg _ (mul_pos d₁0 d₂0)]
no goals
a✝ b✝ c a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * n₂
apply mul_nonneg