proposition: Lemma dec_recip_to_recip `{Field F2} `{!StrongSemiRing_Morphism (f : F → F2)} x Pfx : f (/ x) = // (f x)↾Pfx.
proof: Proof. assert (x ≠ 0). intros Ex. destruct (apart_ne (f x) 0 Pfx). now rewrite Ex, preserves_0. apply (left_cancellation_ne_0 (.*.) (f x)). now apply injective_ne_0. rewrite <-preserves_mult, dec_recip_inverse, reciperse_alt by assumption. now apply preserves_1. 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