proposition: Lemma Z_ring@{} : IsRing Z.
proof: 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.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals