Z_of_N_morphism@{} : IsSemiRingPreserving (cast N Z). Proof. repeat (constructor; try apply _). - intros x y. apply Z_path. red. simpl. ring_with_nat. - intros x y. apply Z_path. red;simpl. ring_with_nat. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.