proposition: Lemma dec_recip_distr (x y: F): / (x * y) = / x * / y.
proof: Proof. destruct (decide (x = 0)) as [Ex|Ex]. rewrite Ex, left_absorb, dec_recip_0. ring. destruct (decide (y = 0)) as [Ey|Ey]. rewrite Ey, right_absorb, dec_recip_0. ring. assert (x * y ≠ 0) as Exy by now apply mult_ne_0. apply (left_cancellation_ne_0 (.*.) (x * y)); trivial. transitivity (x / x * (y / y)). rewrite !dec_recip_inverse by assumption. ring. ring. 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