Z_trivial_apart' `{!TrivialApart N} : TrivialApart Z. Proof. split;[exact _|idtac]. apply (Z_ind2 _). intros [pa na] [pb nb];rewrite Zapart_def;unfold PairT.Tapart;simpl. split;intros E1. - intros E2. apply related_path in E2. red in E2;simpl in E2. apply trivial_apart in E1. auto. - apply trivial_apart. intros E2. apply E1,Z_path. red;simpl. trivial. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.