@[simp]

theorem NNRat.cast_sub {K : Type u_1} [DivisionRing K] [CharZero K] {p q : ℚ≥0} (h : p ≤ q) : ↑(q - p) = ↑q - ↑p