[STATEMENT]
lemma rat_minus_code [code abstract]:
  "quotient_of (p - q) =
    (let (a, c) = quotient_of p; (b, d) = quotient_of q
     in normalize (a * d - b * c, c * d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q in Rat.normalize (a * d - b * c, c * d))
[PROOF STEP]
by (cases p, cases q) (simp add: quotient_of_Fract)