proposition: Lemma dec_recip_negate x : -(/ x) = / (-x).
proof: Proof. destruct (dec (x = 0)) as [Ex|Ex]. - rewrite Ex, negate_0, dec_recip_0, negate_0. reflexivity. - apply (left_cancellation_ne_0 (.*.) (-x)). + apply (snd (flip_negate_ne_0 _)). trivial. + rewrite dec_recip_inverse. * rewrite negate_mult_negate. apply dec_recip_inverse. trivial. * apply (snd (flip_negate_ne_0 _)). trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.fields HoTT.Classes.theory.apartness HoTT.Classes.theory.rings