Theorem isNormalizedMult : forall x y,
  isNormalized x -> isNormalized y -> isNormalized (Rmult x y).
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.
