proposition: Lemma recip_distr_alt (x y : F) Px Py Pxy : // (x * y)↾Pxy = // x↾Px * // y↾Py.
proof: Proof. Proof with try ring. apply (left_cancellation_ne_0 (.*.) (x * y)). now apply apart_ne. transitivity ((x // x↾Px) * (y // y↾Py))... transitivity ((x * y) // (x * y)↾Pxy)... rewrite 3!reciperse_alt... Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids MathClasses.theory.rings