to_ring@{} : T N -> B. Proof. intros p. exact (naturals_to_semiring N B (pos p) - naturals_to_semiring N B (neg p)). Defined.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.