proposition: Lemma dec_recip_negate x : -(/ x) = / (-x).
proof: Proof. destruct (decide (x = 0)) as [Ex|Ex]. now rewrite Ex, negate_0, dec_recip_0, negate_0. apply (left_cancellation_ne_0 (.*.) (-x)). now apply flip_negate_ne_0. rewrite dec_recip_inverse. ring_simplify. now apply dec_recip_inverse. now apply flip_negate_ne_0. Qed.
imports: Coq.setoid_ring.Field Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.fields MathClasses.theory.strong_setoids MathClasses.theory.rings