HOL-ex.Residue_Ring