x y Py : x // (y;Py) = 1 -> x = y. Proof. intros eqxy. rewrite <- (mult_1_r y). rewrite <- eqxy. rewrite (mult_assoc y x (//(y;Py))). rewrite (mult_comm y x). rewrite <- (mult_assoc x y (//(y;Py))). rewrite (recip_inverse (y;Py)). rewrite (mult_1_r x). reflexivity. Qed.
Require Import