proposition: Lemma eqfraction_trans : transitive eqfraction.
proof: Proof. red in |- *. unfold app_rel, eqfraction in |- *. intros x y z H' H'0; try assumption. apply INTEGRAL_DOMAIN_simpl_l with (den y). auto with algebra. apply Trans with (ring_mult (ring_mult (den y) (num x)) (den z)). auto with algebra. apply Trans with (ring_mult (ring_mult (num x) (den y)) (den z)). auto with algebra. apply Trans with (ring_mult (ring_mult (num y) (den x)) (den z)). auto with algebra. apply Trans with (ring_mult (ring_mult (den x) (num y)) (den z)). auto with algebra. apply Trans with (ring_mult (den x) (ring_mult (num y) (den z))). auto with algebra. apply Trans with (ring_mult (den x) (ring_mult (num z) (den y))). auto with algebra. apply Trans with (ring_mult (ring_mult (den x) (num z)) (den y)). auto with algebra. apply Trans with (ring_mult (ring_mult (num z) (den x)) (den y)); auto with algebra. Qed.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util