proposition: Lemma pl_respects : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> equiv (q1 + r1) (q2 + r2).
proof: Proof. unfold equiv;simpl. intros q1 q2 Eq r1 r2 Er. rewrite (plus_assoc _ (neg q2)). rewrite <-(plus_assoc (pos q1)). rewrite (plus_comm (pos r1)). rewrite (plus_assoc (pos q1)). rewrite Eq. rewrite <-(plus_assoc _ (pos r1)). rewrite Er. rewrite plus_assoc. rewrite <-(plus_assoc (pos q2)). rewrite (plus_comm (neg q1)). rewrite !plus_assoc. reflexivity. 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