proposition: Lemma dec_recip_1: / 1 = 1.
proof: Proof. rewrite <-(rings.mult_1_l (/1)). apply dec_recip_inverse. solve_propholds. 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