fact: Definition commringofpadicints := commringquot ( ringcarryequiv p ( isaprimetoneq0 is ) ).
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers