proposition: Lemma dec_recip_swap_r x y: / x * y = / (x / y).
proof: Proof. rewrite dec_recip_distr, involutive. ring. 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