proposition: Lemma recip_proper x y Py : x // (y;Py) = 1 -> x = y.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.apartness HoTT.Classes.theory.rings