apart_cotrans@{} : CoTransitive Tapart. 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.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.