(Z':Type@{U}) `{Integers@{U U U U U U U U} Z'} : forall (P : Rings.Operations -> Type), P (Rings.BuildOperations Z') -> P (Rings.BuildOperations Z). Proof. apply Rings.iso_leibnitz with (integers_to_ring Z' Z);apply _. Qed.
Require Import Require Import Import NatPair.Instances.