proposition: Lemma Frac_dec_mult_num_den x : x = 'num x / 'den x.
proof: Proof. unfold dec_recip, Frac_dec_recip. simpl. case (decide_rel); simpl; intros E. now destruct (den_ne_0 x). unfolds. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings MathClasses.theory.dec_fields