proposition: Lemma apart_respects_aux@{} : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> Tapart q1 r1 -> Tapart q2 r2.
proof: 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.
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