(x : F) (Px : x ≶ 0) : (-//(x;Px))=//(negate_apart(x;Px)). 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.
Require Import