proposition: Lemma recip_proper_alt x y Px Py : x = y → // x↾Px = // y↾Py.
proof: Proof. intro. now apply sm_proper. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids MathClasses.theory.rings