proposition: Lemma recip_proper_alt x y Px Py : x = y -> // (x;Px) = // (y;Py).
proof: Proof. intro E. apply ap. apply Sigma.path_sigma with E. apply path_ishprop. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.apartness HoTT.Classes.theory.rings