apart_respects_aux@{} : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> Tapart q1 r1 -> Tapart q2 r2. Proof. assert (forall q1 q2, equiv q1 q2 -> forall r, Tapart q1 r -> Tapart q2 r) as E. - intros q1 q2 Eq r Er. unfold Tapart,equiv in *. apply (strong_extensionality (+ (neg q1))). assert (Hrw : pos q2 + neg r + neg q1 = (pos q2 + neg q1) + neg r) by ring_with_nat. rewrite Hrw;clear Hrw. rewrite <-Eq. assert (Hrw : pos q1 + neg q2 + neg r = neg q2 + (pos q1 + neg r)) by ring_with_nat. rewrite Hrw;clear Hrw. assert (Hrw : pos r + neg q2 + neg q1 = neg q2 + (pos r + neg q1)) by ring_with_nat;rewrite Hrw;clear Hrw. apply (strong_left_cancellation _ _),Er. - intros ?? Eq ?? Er E'. apply E with q1;trivial. apply symmetry;apply E with r1;apply symmetry;trivial. apply symmetry;trivial. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.