dec_recip_respect@{} : forall q r, equiv q r -> equiv (/ q) (/ r). Proof. unfold equiv,dec_recip,dec_rec;intros q r E;simpl. destruct (decide_rel paths (num q) 0) as [E1|E1], (decide_rel paths (num r) 0) as [E2|E2];simpl. - trivial. - rewrite E1 in E;rewrite mult_0_l in E. destruct E2. apply (right_cancellation_ne_0 mult (den q));try solve_propholds. rewrite mult_0_l;apply symmetry,E. - rewrite E2 in E;rewrite mult_0_l in E. destruct E1. apply (right_cancellation_ne_0 mult (den r));try solve_propholds. rewrite mult_0_l;trivial. - rewrite (mult_comm (den q)), (mult_comm (den r)). apply symmetry, E. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.