proposition: Lemma apart_cotrans@{} : CoTransitive Tapart.
proof: Proof. hnf. unfold Tapart. intros q1 q2 Eq r. apply (strong_left_cancellation (+) (neg r)) in Eq. apply (merely_destruct (cotransitive Eq (pos r + neg q1 + neg q2))); intros [E|E];apply tr. - left. apply (strong_extensionality (+ (neg q2))). assert (Hrw : pos q1 + neg r + neg q2 = neg r + (pos q1 + neg q2)) by ring_with_nat. rewrite Hrw;clear Hrw. trivial. - right. apply (strong_extensionality (+ (neg q1))). assert (Hrw : pos r + neg q2 + neg q1 = pos r + neg q1 + neg q2) by ring_with_nat. rewrite Hrw;clear Hrw. assert (Hrw : pos q2 + neg r + neg q1 = neg r + (pos q2 + neg q1)) by ring_with_nat. rewrite Hrw;clear Hrw. 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