proposition: Lemma addfraction_fun_com : forall x y : fraction_set, Equal (addfraction_fun x y) (addfraction_fun y x).
proof: Proof. unfold addfraction_fun in |- *; simpl in |- *. unfold eqfraction in |- *; simpl in |- *. intros x y; try assumption. apply RING_comp; auto with algebra. Qed.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util