x : -(/ x) = / (-x). 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.
Require Import