proposition: Lemma reciperse_alt (x : F) Px : x // x↾Px = 1.
proof: Proof. now rewrite <-(recip_inverse (x↾Px)). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids MathClasses.theory.rings