proposition: Lemma preserves_recip x Px Pfx : f (// x↾Px) = // (f x)↾Pfx.
proof: Proof. apply (left_cancellation_ne_0 (.*.) (f x)). now apply apart_ne. rewrite <-rings.preserves_mult. rewrite !reciperse_alt. now apply preserves_1. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids MathClasses.theory.rings