proposition: Lemma multfraction_com : forall x y : fraction_set, Equal (multfraction_fun x y) (multfraction_fun y x).
proof: Proof. simpl in |- *. unfold multfraction_fun, eqfraction in |- *; simpl in |- *; auto with algebra. Qed.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util