proposition: Lemma multfraction_dist_l : forall x y z : fraction_set, Equal (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)).
proof: Proof. simpl in |- *. unfold multfraction_fun, eqfraction in |- *; simpl in |- *. intros x y z; try assumption. apply Trans with (ring_mult (ring_mult (num x) (sgroup_law R (ring_mult (num y) (den z)) (ring_mult (num z) (den y)))) (ring_mult (den x) (ring_mult (den y) (ring_mult (den x) (den z))))). auto with algebra. apply Trans with (ring_mult (ring_mult (ring_mult (num x) (sgroup_law R (ring_mult (num y) (den z)) (ring_mult (num z) (den y)))) (den x)) (ring_mult (den y) (ring_mult (den x) (den z)))). auto with algebra. apply RING_comp. apply Trans with (ring_mult (sgroup_law R (ring_mult (num x) (ring_mult (num y) (den z))) (ring_mult (num x) (ring_mult (num z) (den y)))) (den x)). auto with algebra. apply Trans with (sgroup_law R (ring_mult (ring_mult (num x) (ring_mult (num y) (den z))) (den x)) (ring_mult (ring_mult (num x) (ring_mult (num z) (den y))) (den x))). auto with algebra. apply SGROUP_comp. apply Trans with (ring_mult (ring_mult (ring_mult (num x) (num y)) (den z)) (den x)). auto with algebra. apply Trans with (ring_mult (ring_mult (num x) (num y)) (ring_mult (den z) (den x))); auto with algebra. apply Trans with (ring_mult (ring_mult (ring_mult (num x) (num z)) (den y)) (den x)). auto with algebra. apply Trans with (ring_mult (ring_mult (num x) (num z)) (ring_mult (den y) (den x))); auto with algebra. auto with algebra. Qed.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util