fact: Definition isringfuninvmap {X Y : ring} (f : ringiso X Y) : isringfun (invmap f) := isrigfuninvmap f.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids