Add IdempP instances for min_nat and max_nat. Move additional numbers related lemmas and instances into the numbers file.