x Px Pfx : f (// (x;Px)) = // (f x;Pfx). Proof. apply (left_cancellation_ne_0 (.*.) (f x)). - apply apart_ne;trivial. - rewrite <-rings.preserves_mult. rewrite !reciperse_alt. apply preserves_1. Qed.
Require Import