proposition: Lemma ml_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 <-(associativity (num q1)), (associativity (num r1)). rewrite (mult_comm (num r1)), <-(associativity (den q2)), (associativity (num q1)). rewrite Eq, Er. rewrite <-(associativity (num q2)), (associativity (den q1)), (mult_comm (den q1)). rewrite <-(simple_associativity (num r2)), <-(simple_associativity (num q2)). reflexivity. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields