(x y : F) Px Py Pxy : // (x * y ; Pxy) = // (x;Px) * // (y;Py). Proof. apply (left_cancellation_ne_0 (.*.) (x * y)). - apply apart_ne;trivial. - transitivity ((x // (x;Px)) * (y // (y;Py))). + rewrite 3!reciperse_alt,mult_1_r. reflexivity. + rewrite <-simple_associativity,<-simple_associativity. apply ap. rewrite simple_associativity. rewrite (commutativity (f:=mult) _ y). rewrite <-simple_associativity. reflexivity. Qed.
Require Import