Z_ring@{} : IsCRing Z. Proof. repeat split. 1,8: exact _. all: first [change sg_op with mult; change mon_unit with 1 | change sg_op with plus; change mon_unit with 0]; hnf. - apply (Z_ind3 _). intros a b c;apply Z_path;red;simpl. rewrite !plus_assoc. reflexivity. - apply (Z_ind _). intros a;apply Z_path;red;simpl. rewrite !plus_0_l. reflexivity. - apply (Z_ind _). intros a;apply Z_path;red;simpl. rewrite !plus_0_r. reflexivity. - apply (Z_ind _). intros a;apply Z_path;red;simpl. rewrite plus_0_l,plus_0_r. apply plus_comm. - apply (Z_ind _). intros a;apply Z_path;red;simpl. rewrite plus_0_l,plus_0_r. apply plus_comm. - apply (Z_ind2 _). intros a b;apply Z_path;red;simpl. apply ap011;apply plus_comm. - apply (Z_ind3 _). intros [pa na] [pb nb] [pc nc];apply Z_path;red;simpl. ring_with_nat. - apply (Z_ind _). intros;apply Z_path;red;simpl. ring_with_nat. - apply (Z_ind _). intros;apply Z_path;red;simpl. ring_with_nat. - apply (Z_ind2 _). intros;apply Z_path;red;simpl. ring_with_nat. - apply (Z_ind3 _). intros [pa na] [pb nb] [pc nc];apply Z_path;red;simpl. ring_with_nat. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.