proposition: Lemma recip_negate (x : F) (Px : x ≶ 0) : (-//(x;Px))=//(negate_apart(x;Px)).
proof: Proof. apply (left_cancellation (.*.) x). rewrite <- negate_mult_distr_r. rewrite reciperse_alt. apply flip_negate. rewrite negate_mult_distr_l. refine (_^). apply reciperse_alt. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.apartness HoTT.Classes.theory.rings