{A B : Type} `{Plus A, Plus B, Mult A, Mult B, Zero A, Zero B, One A, One B} {f : A -> B} : _ <~> IsSemiRingPreserving f := ltac:(issig).
Require Import Spaces.Nat.Core. Require Import Modalities.ReflectiveSubuniverse.