proposition: Lemma dec_recip_respect@{} : forall q r, equiv q r -> equiv (/ q) (/ r).
proof: 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.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields