proposition: Lemma ml_respects : forall q1 q2, equiv q1 q2 -> forall r1 r2, equiv r1 r2 -> equiv (q1 * r1) (q2 * r2).
proof: 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.
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