pl_respect@{} : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> equiv (q1 + r1) (q2 + r2). Proof. unfold equiv;intros q1 q2 Eq r1 r2 Er. simpl. rewrite plus_mult_distr_r. rewrite <-(associativity (num q1) (den r1)). rewrite (associativity (den r1)), (mult_comm (den r1)), <-(associativity (den q2)). rewrite (associativity (num q1)), Eq. rewrite (mult_comm (den q2)), <-(associativity (num r1)), (associativity (den q1)). rewrite (mult_comm (den q1)), <-(associativity (den r2)), (associativity (num r1)). rewrite Er. rewrite (mult_comm (den r1)), <-(associativity (num q2)), (associativity (den q1)). rewrite (mult_comm (den q1)), <-(associativity (den r2)), (associativity (num q2)). rewrite <-(associativity (num r2)), (associativity (den r1)), (mult_comm _ (den q2)). rewrite (mult_comm (den r1)), (associativity (num r2)). apply symmetry;apply plus_mult_distr_r. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.