proposition: Lemma eqfraction_num0 : forall x : fraction, Equal (num x) (monoid_unit R) -> eqfraction x fraction0.
proof: Proof. intros x; try assumption. case x; unfold eqfraction, fraction0 in |- *; simpl in |- *. intros numer denom H' H'0; try assumption. apply Trans with numer; auto with algebra. apply Trans with (monoid_unit R); auto with algebra. Qed.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util