proposition: Lemma preserves_recip x Px Pfx : f (// (x;Px)) = // (f x;Pfx).
proof: Proof. apply (left_cancellation_ne_0 (.*.) (f x)). - apply apart_ne;trivial. - rewrite <-rings.preserves_mult. rewrite !reciperse_alt. apply preserves_1. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.apartness HoTT.Classes.theory.rings