case a.num
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).num = (↑q).num

case a.den
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).den = (↑q).den
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ p = q
ext
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑p).num

p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑q).num
case a.num
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).num = (↑q).num
apply (Int.natAbs_inj_of_nonneg_of_nonneg _ _).1 hn
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑q).num
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑p).num

p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑q).num
exact Rat.num_nonneg_iff_zero_le.2 p.2
no goals
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑q).num
exact Rat.num_nonneg_iff_zero_le.2 q.2
no goals
case a.den
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).den = (↑q).den
exact hd