proposition: Lemma eqfraction0 : forall x : fraction, eqfraction x fraction0 -> Equal (num x) (monoid_unit R).
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 (ring_mult numer (ring_unit R)); auto with algebra. apply Trans with (ring_mult (monoid_unit R) denom); auto with algebra. Qed.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util