proposition: Lemma pl_respect@{} : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> equiv (q1 + r1) (q2 + r2).
proof: 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.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields