Z_is_apart' : IsApart Z. Proof. split. - apply _. - apply _. - hnf. apply (Z_ind2 (fun _ _ => _ -> _)). intros [pa na] [pb nb];rewrite !Zapart_def;unfold PairT.Tapart;simpl. apply symmetry. - hnf. intros x y E z;revert x y z E. apply (Z_ind3 (fun _ _ _ => _ -> _)). intros a b c;rewrite !Zapart_def;unfold PairT.Tapart;simpl. intros E1. apply (strong_left_cancellation (+) (PairT.neg c)) in E1. eapply (merely_destruct (cotransitive E1 _));intros [E2|E2];apply tr. + left. apply (strong_extensionality (+ (PairT.neg b))). assert (Hrw : PairT.pos a + PairT.neg c + PairT.neg b = PairT.neg c + (PairT.pos a + PairT.neg b)) by ring_with_nat;rewrite Hrw;exact E2. + right. apply (strong_extensionality (+ (PairT.neg a))). assert (Hrw : PairT.pos c + PairT.neg b + PairT.neg a = PairT.pos c + PairT.neg a + PairT.neg b) by ring_with_nat;rewrite Hrw;clear Hrw. assert (Hrw : PairT.pos b + PairT.neg c + PairT.neg a = PairT.neg c + (PairT.pos b + PairT.neg a)) by ring_with_nat;rewrite Hrw;clear Hrw. trivial. - apply (Z_ind2 _). intros a b;rewrite Zapart_def;unfold PairT.Tapart. split;intros E. + apply Z_path;red. apply tight_apart,E. + apply related_path in E. apply tight_apart,E. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.