{A B : Ring} : RingIsomorphism A B -> RingIsomorphism B A. Proof. intros [f e]. snrapply Build_RingIsomorphism. { snrapply Build_RingHomomorphism. 1: exact f^-1. exact _. } exact _. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.