proposition: Lemma dec_recip_correct (x : F) Px : / x = // x↾Px.
proof: Proof. Proof with auto. apply (left_cancellation_ne_0 (.*.) x). now apply trivial_apart. now rewrite dec_recip_inverse, reciperse_alt by now apply trivial_apart. Qed.
imports: Coq.setoid_ring.Field Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.fields MathClasses.theory.strong_setoids MathClasses.theory.rings