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