proposition: Lemma Frac_nonzero_num x : x ≠ 0 ↔ num x ≠ 0.
proof: Proof. split; intros E F; apply E; unfolds. rewrite F. ring. rewrite right_identity in F. rewrite F. apply left_absorb. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings MathClasses.theory.dec_fields