forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> equiv (q1 * r1) (q2 * r2). Proof. intros q1 q2 Eq r1 r2 Er. transitivity (q1 * r2);unfold equiv in *;simpl. - transitivity (pos q1 * (pos r1 + neg r2) + neg q1 * (neg r1 + pos r2)). + rewrite 2!plus_mult_distr_l. rewrite <-2!plus_assoc. apply ap. rewrite 2!plus_assoc. rewrite (plus_comm (neg q1 * neg r1)). reflexivity. + rewrite Er. rewrite plus_mult_distr_l. rewrite (plus_comm (neg r1)). rewrite <-Er. rewrite plus_mult_distr_l. rewrite <-2!plus_assoc. apply ap. rewrite (plus_comm (neg q1 * pos r1)). rewrite 2!plus_assoc. rewrite (plus_comm (pos q1 * neg r1)). reflexivity. - transitivity ((pos q1 + neg q2) * pos r2 + (neg q1 + pos q2) * neg r2). + rewrite 2!plus_mult_distr_r. rewrite <-2!plus_assoc;apply ap. rewrite (plus_comm (pos q2 * neg r2)). rewrite 2!plus_assoc. rewrite (plus_comm (neg q1 * neg r2)). reflexivity. + rewrite Eq,plus_mult_distr_r. rewrite (plus_comm (neg q1)),<-Eq,plus_mult_distr_r. rewrite <-2!plus_assoc. apply ap. rewrite plus_assoc,(plus_comm (neg q1 * pos r2)). apply plus_comm. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.