case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ toNNRat (p * q) = toNNRat p * toNNRat q

case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
p q : ℚ
hp : 0 ≤ p
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
cases' le_total 0 q with hq hq
no goals
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
ext <;> simp [toNNRat, hp, hq, max_eq_left, mul_nonneg]
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
no goals
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]