proposition: Lemma Z_trivial_apart' `{!TrivialApart N} : TrivialApart Z.
proof: 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.
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