proposition: Lemma addfraction_law : fun2_compatible addfraction_fun.
proof: Proof. red in |- *. intros x x' y y' H' H'0; try assumption. apply Trans with (addfraction_fun x' y). apply addfraction_law_l; auto with algebra. apply addfraction_law_r; auto with algebra. Qed.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util