Some exiled lemmas about casting #
These lemmas have been removed from Mathlib.Data.Rat.Cast.Defs
to avoiding needing to import Mathlib.Algebra.Field.Basic
there.
In fact, these lemmas don't appear to be used anywhere in Mathlib, so perhaps this file can simply be deleted.