(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Automatic Coercions Import.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Integral_domain_facts.
Require Export Cfield_cat.
Require Export Abelian_group_facts.
Require Export Ring_util.
(** Title "The field of fractions of an integral domain" "with decidable equality." *)
Section Def.
Variable R : INTEGRAL_DOMAIN.
Variable diff10 : ~ Equal (ring_unit R) (monoid_unit R).
Set Strict Implicit.
Unset Implicit Arguments.

Record fraction : Type := 
  {num : R; den : R; den_prf : ~ Equal den (monoid_unit R)}.
Set Implicit Arguments.
Unset Strict Implicit.
Hint Resolve den_prf: algebra.

Definition eqfraction (x y : fraction) :=
  Equal (ring_mult (num x) (den y)) (ring_mult (num y) (den x)).

Lemma eqfraction_refl : reflexive eqfraction.
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
intros x; red in |- *.
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
Qed.

Definition fraction0 := Build_fraction (monoid_unit R) (ring_unit R) diff10.

Lemma eqfraction0 :
 forall x : fraction, eqfraction x fraction0 -> Equal (num x) (monoid_unit R).
(* Goal: forall (x : fraction) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x)))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end))) *)
intros x; try assumption.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))), eqfraction x fraction0 *)
case x; unfold eqfraction, fraction0 in |- *; simpl in |- *.
(* Goal: forall (num den : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) den (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) num (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) num (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) den) *)
intros numer denom H' H'0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult numer (ring_unit R)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (monoid_unit R) denom); auto with algebra.
Qed.

Lemma eqfraction_num0 :
 forall x : fraction, Equal (num x) (monoid_unit R) -> eqfraction x fraction0.
(* Goal: forall (x : fraction) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x)))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end))) *)
intros x; try assumption.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))), eqfraction x fraction0 *)
case x; unfold eqfraction, fraction0 in |- *; simpl in |- *.
(* Goal: forall (num den : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) den (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) num (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) num (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) den) *)
intros numer denom H' H'0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with numer; auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (monoid_unit R); auto with algebra.
Qed.

Lemma eqfraction_sym : symmetric eqfraction.
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
unfold app_rel, eqfraction in |- *; auto with algebra.
Qed.

Lemma eqfraction_trans : transitive eqfraction.
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: forall (x y z : fraction) (_ : @app_rel fraction eqfraction x y) (_ : @app_rel fraction eqfraction y z), @app_rel fraction eqfraction x z *)
unfold app_rel, eqfraction in |- *.
(* Goal: forall (x y z : fraction) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x)) *)
intros x y z H' H'0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x)) *)
apply INTEGRAL_DOMAIN_simpl_l with (den y).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x))) *)
apply Trans with (ring_mult (ring_mult (den y) (num x)) (den z)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (num x)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x))) *)
apply Trans with (ring_mult (ring_mult (num x) (den y)) (den z)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x))) *)
apply Trans with (ring_mult (ring_mult (num y) (den x)) (den z)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x))) *)
apply Trans with (ring_mult (ring_mult (den x) (num y)) (den z)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (num y)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x))) *)
apply Trans with (ring_mult (den x) (ring_mult (num y) (den z))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x))) *)
apply Trans with (ring_mult (den x) (ring_mult (num z) (den y))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den x))) *)
apply Trans with (ring_mult (ring_mult (den x) (num z)) (den y)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
apply Trans with (ring_mult (ring_mult (num z) (den x)) (den y));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
Qed.

Definition fraction_set : SET.
(* Goal: Ob SET *)
apply (Build_Setoid (Carrier:=fraction) (Equal:=eqfraction)).
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: and (@transitive fraction eqfraction) (@symmetric fraction eqfraction) *)
split; [ try assumption | idtac ].
(* Goal: @reflexive fraction eqfraction *)
(* Goal: @partial_equivalence fraction eqfraction *)
exact eqfraction_refl.
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: and (@transitive fraction eqfraction) (@symmetric fraction eqfraction) *)
split; [ try assumption | idtac ].
(* Goal: @transitive fraction eqfraction *)
(* Goal: @symmetric fraction eqfraction *)
exact eqfraction_trans.
(* Goal: @symmetric fraction eqfraction *)
exact eqfraction_sym.
Defined.

Definition addfraction_fun (x y : fraction_set) : fraction_set :=
  Build_fraction
    (sgroup_law R (ring_mult (num x) (den y)) (ring_mult (num y) (den x)))
    (ring_mult (den x) (den y))
    (INTEGRAL_DOMAIN_prop_rev (den_prf x) (den_prf y)).

Definition opfraction_fun (x : fraction_set) : fraction_set :=
  Build_fraction (group_inverse R (num x)) (den x) (den_prf x).

Definition multfraction_fun (x y : fraction_set) : fraction_set :=
  Build_fraction (ring_mult (num x) (num y)) (ring_mult (den x) (den y))
    (INTEGRAL_DOMAIN_prop_rev (den_prf x) (den_prf y)).

Definition fraction1 : fraction_set :=
  Build_fraction (ring_unit R) (ring_unit R) diff10.

Lemma addfraction_law_l :
 forall x x' y : fraction_set,
 Equal x x' -> Equal (addfraction_fun x y) (addfraction_fun x' y).
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
unfold addfraction_fun in |- *; simpl in |- *.
(* Goal: not (eqfraction (ring_unit fract_field_ring_aux) fraction0) *)
unfold eqfraction in |- *; simpl in |- *.
(* Goal: forall (x x' y : fraction) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den x))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (den x') (den y))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
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)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
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)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (@ring_mult (cring_ring (idomain_ring R)) (den y) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z))) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
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'))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
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))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
apply SGROUP_comp.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (den y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
apply Trans with (ring_mult (ring_mult (den y) (num x)) (den x')).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (num x)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (den y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
apply Trans with (ring_mult (ring_mult (den y) (num x')) (den x)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (num x)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (num x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (num x')) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (den y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
apply Trans with (ring_mult (den y) (ring_mult (num x) (den x'))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (den y) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (num x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (num x')) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (den y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
apply Trans with (ring_mult (den y) (ring_mult (num x') (den x))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (den y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
apply Trans with (ring_mult (num y) (ring_mult (den x) (den x'))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x')) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (den y) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (den x)) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x'))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
apply Trans with (ring_mult (num y) (ring_mult (den x') (den x))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
Qed.

Lemma addfraction_fun_com :
 forall x y : fraction_set, Equal (addfraction_fun x y) (addfraction_fun y x).
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
unfold addfraction_fun in |- *; simpl in |- *.
(* Goal: not (eqfraction (ring_unit fract_field_ring_aux) fraction0) *)
unfold eqfraction in |- *; simpl in |- *.
(* Goal: forall (x y : fraction) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end) (den match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end)) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) *)
intros x y; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply RING_comp; auto with algebra.
Qed.

Lemma addfraction_law_r :
 forall x y y' : fraction_set,
 Equal y y' -> Equal (addfraction_fun x y) (addfraction_fun x y').
(* Goal: forall (x y y' : Carrier fraction_set) (_ : @Equal fraction_set y y'), @Equal fraction_set (addfraction_fun x y) (addfraction_fun x y') *)
intros x y y' H'; try assumption.
(* Goal: @Equal fraction_set (addfraction_fun x y) (addfraction_fun x y') *)
apply Trans with (addfraction_fun y x).
(* Goal: @Equal fraction_set (addfraction_fun y' x) (addfraction_fun x y') *)
apply addfraction_fun_com.
(* Goal: @Equal fraction_set (addfraction_fun y x) (addfraction_fun x y') *)
apply Trans with (addfraction_fun y' x).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply addfraction_law_l; auto with algebra.
(* Goal: @Equal fraction_set (addfraction_fun y' x) (addfraction_fun x y') *)
apply addfraction_fun_com.
Qed.

Lemma addfraction_law : fun2_compatible addfraction_fun.
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: forall (x x' y y' : fraction) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den x))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den y')) (@ring_mult (cring_ring (idomain_ring R)) (num y') (den y))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num y)) (@ring_mult (cring_ring (idomain_ring R)) (den x') (den y'))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (num y')) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
intros x x' y y' H' H'0; try assumption.
(* Goal: @Equal fraction_set (addfraction_fun x y) (addfraction_fun x' y') *)
apply Trans with (addfraction_fun x' y).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply addfraction_law_l; auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply addfraction_law_r; auto with algebra.
Qed.

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)).
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold multfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
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))))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
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)))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (@ring_mult (cring_ring (idomain_ring R)) (den y) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z))) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
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)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
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))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
apply SGROUP_comp.
apply
 Trans
  with (ring_mult (ring_mult (ring_mult (num x) (num y)) (den z)) (den x)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
apply
 Trans
  with (ring_mult (ring_mult (num x) (num y)) (ring_mult (den z) (den x)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
apply
 Trans
  with (ring_mult (ring_mult (ring_mult (num x) (num z)) (den y)) (den x)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
apply
 Trans
  with (ring_mult (ring_mult (num x) (num z)) (ring_mult (den y) (den x)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
Qed.

Lemma multfraction_com :
 forall x y : fraction_set,
 Equal (multfraction_fun x y) (multfraction_fun y x).
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
unfold multfraction_fun, eqfraction in |- *; simpl in |- *; auto with algebra.
Qed.

Definition fract_field_ring_aux : RING.
apply
 (BUILD_RING (E:=fraction_set) (ringplus:=addfraction_fun)
    (ringmult:=multfraction_fun) (zero:=fraction0) (un:=fraction1)
    (ringopp:=opfraction_fun)).
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (addfraction_fun x y) (addfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (addfraction_fun (addfraction_fun x y) z) (addfraction_fun x (addfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
exact addfraction_law.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold addfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
intros x y z; try assumption.
apply
 Trans
  with
    (ring_mult
       (sgroup_law R
          (ring_mult
             (sgroup_law R (ring_mult (num x) (den y))
                (ring_mult (num y) (den x))) (den z))
          (ring_mult (num z) (ring_mult (den x) (den y))))
       (ring_mult (ring_mult (den x) (den y)) (den z))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (@ring_mult (cring_ring (idomain_ring R)) (den y) (den z))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z))) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
apply RING_comp.
apply
 Trans
  with
    (sgroup_law R
       (sgroup_law R (ring_mult (ring_mult (num x) (den y)) (den z))
          (ring_mult (ring_mult (num y) (den x)) (den z)))
       (ring_mult (num z) (ring_mult (den x) (den y)))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
apply
 Trans
  with
    (sgroup_law R (ring_mult (ring_mult (num x) (den y)) (den z))
       (sgroup_law R (ring_mult (ring_mult (num y) (den x)) (den z))
          (ring_mult (num z) (ring_mult (den x) (den y))))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
apply SGROUP_comp.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
apply
 Trans
  with
    (sgroup_law R (ring_mult (ring_mult (num y) (den z)) (den x))
       (ring_mult (ring_mult (num z) (den y)) (den x))).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (den x)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y)) (den x))) (@ring_mult (cring_ring (idomain_ring R)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (num z) (den y))) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (den z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x fraction0) x *)
(* Goal: forall (x y : Carrier fraction_set) (_ : @Equal fraction_set x y), @Equal fraction_set (opfraction_fun x) (opfraction_fun y) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
apply SGROUP_comp.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
apply Trans with (ring_mult (num z) (ring_mult (den y) (den x)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold addfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall (x : fraction) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x)))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end))) *)
intros x; try assumption.
apply Trans with (ring_mult (sgroup_law R (num x) (monoid_unit R)) (den x));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold opfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall (x y : fraction) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (group_inverse (abelian_group_group (ring_group (cring_ring (idomain_ring R)))) (num x)) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (group_inverse (abelian_group_group (ring_group (cring_ring (idomain_ring R)))) (num y)) (den x)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (addfraction_fun x (opfraction_fun x)) fraction0 *)
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
intros x y H'; try assumption.
apply Trans with (group_inverse R (ring_mult (num x) (den y)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
apply Trans with (group_inverse R (ring_mult (num y) (den x)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold addfraction_fun, opfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall (x : fraction) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x)))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end))) *)
intros x; try assumption.
apply
 Trans
  with
    (sgroup_law R (ring_mult (num x) (den x))
       (ring_mult (group_inverse R (num x)) (den x))); 
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
apply
 Trans
  with (ring_mult (sgroup_law R (num x) (group_inverse R (num x))) (den x));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (monoid_unit R) (den x)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (monoid_unit R); auto with algebra.
(* Goal: forall x y : Carrier fraction_set, @Equal fraction_set (addfraction_fun x y) (addfraction_fun y x) *)
(* Goal: forall (x x' y y' : Carrier fraction_set) (_ : @Equal fraction_set x x') (_ : @Equal fraction_set y y'), @Equal fraction_set (multfraction_fun x y) (multfraction_fun x' y') *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
exact addfraction_fun_com.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold multfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall (x x' y y' : fraction) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den x')) (@ring_mult (cring_ring (idomain_ring R)) (num x') (den x))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den y')) (@ring_mult (cring_ring (idomain_ring R)) (num y') (den y))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num y)) (@ring_mult (cring_ring (idomain_ring R)) (den x') (den y'))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x') (num y')) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y))) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (multfraction_fun x y) z) (multfraction_fun x (multfraction_fun y z)) *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun x fraction1) x *)
(* Goal: forall x : Carrier fraction_set, @Equal fraction_set (multfraction_fun fraction1 x) x *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
intros x x' y y' H' H'0; try assumption.
apply
 Trans
  with (ring_mult (ring_mult (num x) (den x')) (ring_mult (num y) (den y')));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
apply
 Trans
  with (ring_mult (ring_mult (num x') (den x)) (ring_mult (num y') (den y)));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold multfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold multfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: forall (x : fraction) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x)))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end))) *)
intros x; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (multfraction_fun x fraction1); auto with algebra.
(* Goal: @Equal fraction_set (multfraction_fun z y) (multfraction_fun y z) *)
apply multfraction_com.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold multfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold multfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun x (addfraction_fun y z)) (addfraction_fun (multfraction_fun x y) (multfraction_fun x z)) *)
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
exact multfraction_dist_l.
(* Goal: forall x y z : Carrier fraction_set, @Equal fraction_set (multfraction_fun (addfraction_fun x y) z) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
intros x y z; try assumption.
apply Trans with (multfraction_fun z (addfraction_fun x y));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: @Equal fraction_set (multfraction_fun z y) (multfraction_fun y z) *)
apply multfraction_com.
apply
 Trans with (addfraction_fun (multfraction_fun z x) (multfraction_fun z y));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
 auto with algebra.
(* Goal: @Equal fraction_set (multfraction_fun z (addfraction_fun x y)) (addfraction_fun (multfraction_fun z x) (multfraction_fun z y)) *)
(* Goal: @Equal fraction_set (addfraction_fun (multfraction_fun z x) (multfraction_fun z y)) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
apply multfraction_dist_l.
(* Goal: @Equal fraction_set (addfraction_fun (multfraction_fun z x) (multfraction_fun z y)) (addfraction_fun (multfraction_fun x z) (multfraction_fun y z)) *)
apply addfraction_law.
(* Goal: @Equal fraction_set (multfraction_fun z y) (multfraction_fun y z) *)
apply multfraction_com.
(* Goal: @Equal fraction_set (multfraction_fun z y) (multfraction_fun y z) *)
apply multfraction_com.
Defined.

Definition fract_field_ring : CRING.
(* Goal: Ob CRING *)
apply (Build_cring (cring_ring:=fract_field_ring_aux)).
(* Goal: cring_on fract_field_ring_aux *)
apply (Build_cring_on (R:=fract_field_ring_aux)).
(* Goal: @commutative (sgroup_set (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group fract_field_ring_aux))))) (@ring_mult_sgroup (ring_group fract_field_ring_aux) (ring_on_def fract_field_ring_aux))) (@ring_mult_monoid (ring_group fract_field_ring_aux) (ring_on_def fract_field_ring_aux))))) (@sgroup_law_map (sgroup_set (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group fract_field_ring_aux))))) (@ring_mult_sgroup (ring_group fract_field_ring_aux) (ring_on_def fract_field_ring_aux))) (@ring_mult_monoid (ring_group fract_field_ring_aux) (ring_on_def fract_field_ring_aux))))) (sgroup_on_def (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group fract_field_ring_aux))))) (@ring_mult_sgroup (ring_group fract_field_ring_aux) (ring_on_def fract_field_ring_aux))) (@ring_mult_monoid (ring_group fract_field_ring_aux) (ring_on_def fract_field_ring_aux)))))) *)
exact multfraction_com.
Defined.
Variable
  zero_dec :
    forall x : R, {Equal x (monoid_unit R)} + {~ Equal x (monoid_unit R)}.

Definition invfraction_fun : fract_field_ring -> fract_field_ring :=
  fun x : fraction_set =>
  match zero_dec (num x) with
  | left _ => x
  | right n => Build_fraction (den x) (num x) n
  end.

Definition invfraction : MAP fract_field_ring fract_field_ring.
apply
 (Build_Map (A:=fract_field_ring) (B:=fract_field_ring) (Ap:=invfraction_fun)).
(* Goal: @fun_compatible (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction_fun *)
red in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold invfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall (x y : fraction) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end) (den match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end)) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) *)
intros x y; try assumption.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (den x)), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end) (den match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end)) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) *)
case (zero_dec (num x)); intros.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end)) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end) (den (Build_fraction (den x) (num x) n))) *)
case (zero_dec (num y)); intros.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num y)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end)) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end) (den (Build_fraction (den x) (num x) n))) *)
cut (Equal (den x) (monoid_unit R)).
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (ring_unit (cring_ring (idomain_ring R)))), False *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num y)) (@ring_mult (cring_ring (idomain_ring R)) (den y) (den x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end)) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (monoid_unit R) (num y)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (monoid_unit R); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (den y) (monoid_unit R)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply INTEGRAL_DOMAIN_mult_n0_l with (num y); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (num x) (den y)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (monoid_unit R) (den y)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end)) (@ring_mult (cring_ring (idomain_ring R)) (num match zero_dec (num y) with | left e => y | right n => Build_fraction (den y) (num y) n end) (den (Build_fraction (den x) (num x) n))) *)
case (zero_dec (num y)); intros.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
cut (Equal (den y) (monoid_unit R)).
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (ring_unit (cring_ring (idomain_ring R)))), False *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den y)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (monoid_unit R) (num x)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (monoid_unit R); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (den x) (monoid_unit R)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply INTEGRAL_DOMAIN_mult_n0_l with (num x); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (num y) (den x)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (monoid_unit R) (den x)); auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (num y) (den x)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (num x) (den y)); auto with algebra.
Defined.

Let ff_inr_r :
  forall x : fract_field_ring,
  ~ Equal x (monoid_unit fract_field_ring) ->
  Equal (ring_mult x (Ap invfraction x)) (ring_unit fract_field_ring).
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
unfold invfraction_fun, eqfraction in |- *; simpl in |- *.
(* Goal: forall (x : fraction) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x)))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end))) *)
intros x; try assumption.
(* Goal: forall _ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num x) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den x))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (num match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (den match zero_dec (num x) with | left e => x | right n => Build_fraction (den x) (num x) n end))) *)
case (zero_dec (num x)); simpl in |- *; intros.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
absurd (Equal (num x) (monoid_unit R)); auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den x)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (num x))) *)
intuition.
(* Goal: False *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@ring_mult (cring_ring (idomain_ring R)) (num x) (den x)) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (@ring_mult (cring_ring (idomain_ring R)) (den x) (num x))) *)
apply H.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (num x); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (monoid_unit R); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (num x) (den x)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (den x) (num x)); auto with algebra.
Qed.

Hint Resolve ff_inr_r: algebra.

Let ff_field_on : field_on fract_field_ring.
(* Goal: field_on (cring_ring fract_field_ring) *)
apply (Build_field_on (R:=fract_field_ring) (field_inverse_map:=invfraction)).
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (@ring_mult (cring_ring fract_field_ring) x (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction x)) (ring_unit (cring_ring fract_field_ring)) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (@ring_mult (cring_ring fract_field_ring) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction x) x) (ring_unit (cring_ring fract_field_ring)) *)
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
exact ff_inr_r.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (@ring_mult (cring_ring fract_field_ring) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) invfraction x) x) (ring_unit (cring_ring fract_field_ring)) *)
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
intros x H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult x (Ap invfraction x)); auto with algebra.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring)))))) (ring_unit (cring_ring fract_field_ring)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring fract_field_ring))))))) *)
simpl in |- *.
(* Goal: not (eqfraction (ring_unit fract_field_ring_aux) fraction0) *)
unfold eqfraction in |- *; simpl in |- *.
(* Goal: not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (ring_unit (cring_ring (idomain_ring R))))) *)
unfold not in |- *.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (ring_unit (cring_ring (idomain_ring R))) (ring_unit (cring_ring (idomain_ring R)))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (ring_unit (cring_ring (idomain_ring R)))), False *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
absurd (Equal (ring_unit R:R) (monoid_unit R)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (ring_unit R) (ring_unit R)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (num x)) (@ring_mult (cring_ring (idomain_ring R)) (num y) (num x)) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (den y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R)))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) *)
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring (idomain_ring R))))))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den x) (num x) n)) (den (Build_fraction (den y) (num y) n0))) (@ring_mult (cring_ring (idomain_ring R)) (num (Build_fraction (den y) (num y) n0)) (den (Build_fraction (den x) (num x) n))) *)
apply Trans with (ring_mult (monoid_unit R) (ring_unit R)); auto with algebra.
Defined.

Definition fraction_cfield := Build_cfield ff_field_on.
End Def.
