(* 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 Implicit Arguments.
Unset Strict Implicit.
Require Export Ring_cat.
Require Export Group_facts.
Require Export Abelian_group_facts.
(** Title "Basic properties of rings." *)
Section Lemmas.
Variable R : RING.

Lemma RING_assoc :
 forall x y z : R,
 Equal (ring_mult (ring_mult x y) z) (ring_mult x (ring_mult y z)).
(* Goal: forall x y z : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (@ring_mult R x y) z) (@ring_mult R x (@ring_mult R y z)) *)
exact (sgroup_assoc_prf (E:=R) (ring_monoid R)).
Qed.

Lemma RING_comp :
 forall x x' y y' : R,
 Equal x x' -> Equal y y' -> Equal (ring_mult x y) (ring_mult x' y').
(* Goal: forall (x x' y y' : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x') (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) y y'), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x y) (@ring_mult R x' y') *)
unfold ring_mult in |- *; auto with algebra.
Qed.

Lemma RING_unit_r : forall x : R, Equal (ring_mult x (ring_unit R)) x.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (ring_unit R)) x *)
exact (monoid_unit_r_prf (ring_monoid R)).
Qed.

Lemma RING_unit_l : forall x : R, Equal (ring_mult (ring_unit R) x) x.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (ring_unit R) x) x *)
exact (monoid_unit_l_prf (ring_monoid R)).
Qed.

Lemma RING_dist_r :
 forall x y z : R,
 Equal (ring_mult (sgroup_law R x y) z)
   (sgroup_law R (ring_mult x z) (ring_mult y z)).
(* Goal: forall x y z : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) x y) z) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@ring_mult R x z) (@ring_mult R y z)) *)
exact (ring_dist_r_prf R).
Qed.

Lemma RING_dist_l :
 forall x y z : R,
 Equal (ring_mult x (sgroup_law R y z))
   (sgroup_law R (ring_mult x y) (ring_mult x z)).
(* Goal: forall x y z : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) y z)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@ring_mult R x y) (@ring_mult R x z)) *)
exact (ring_dist_l_prf R).
Qed.
Hint Resolve RING_assoc RING_comp RING_unit_r RING_unit_l RING_dist_r
  RING_dist_l: algebra.

Lemma RING_absorbant_r :
 forall x : R, Equal (ring_mult x (monoid_unit R)) (monoid_unit R).
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) *)
intros x; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R)))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) *)
apply GROUP_reg_right with (ring_mult x (monoid_unit R)).
apply Trans with (ring_mult x (sgroup_law R (monoid_unit R) (monoid_unit R)));
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) y (group_inverse (abelian_group_group (ring_group R)) y))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) *)
apply Trans with (ring_mult x (monoid_unit R)); auto with algebra.
Qed.
Hint Resolve RING_absorbant_r: algebra.

Lemma RING_absorbant_l :
 forall x : R, Equal (ring_mult (monoid_unit R) x) (monoid_unit R).
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) *)
intros x; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) *)
apply GROUP_reg_right with (ring_mult (monoid_unit R) x).
apply Trans with (ring_mult (sgroup_law R (monoid_unit R) (monoid_unit R)) x);
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R)))))) x) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) x)) *)
apply Trans with (ring_mult (monoid_unit R) x); auto with algebra.
Qed.
Hint Resolve RING_absorbant_l: algebra.

Lemma RING_op_mult_l :
 forall x y : R,
 Equal (ring_mult (group_inverse R x) y) (group_inverse R (ring_mult x y)).
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (group_inverse (abelian_group_group (ring_group R)) y)) (group_inverse (abelian_group_group (ring_group R)) (@ring_mult R x y)) *)
intros x y; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (group_inverse (abelian_group_group (ring_group R)) y)) (group_inverse (abelian_group_group (ring_group R)) (@ring_mult R x y)) *)
apply Sym.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) (@ring_mult R x y)) (@ring_mult R x (group_inverse (abelian_group_group (ring_group R)) y)) *)
apply GROUP_law_inverse.
apply Trans with (ring_mult (sgroup_law R x (group_inverse R x)) y);
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) x (group_inverse (abelian_group_group (ring_group R)) x)) y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) *)
apply Trans with (ring_mult (monoid_unit R) y); auto with algebra.
Qed.
Hint Resolve RING_op_mult_l: algebra.

Lemma RING_op_mult_r :
 forall x y : R,
 Equal (ring_mult x (group_inverse R y)) (group_inverse R (ring_mult x y)).
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (group_inverse (abelian_group_group (ring_group R)) y)) (group_inverse (abelian_group_group (ring_group R)) (@ring_mult R x y)) *)
intros x y; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (group_inverse (abelian_group_group (ring_group R)) y)) (group_inverse (abelian_group_group (ring_group R)) (@ring_mult R x y)) *)
apply Sym.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) (@ring_mult R x y)) (@ring_mult R x (group_inverse (abelian_group_group (ring_group R)) y)) *)
apply GROUP_law_inverse.
apply Trans with (ring_mult x (sgroup_law R y (group_inverse R y)));
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R x (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) y (group_inverse (abelian_group_group (ring_group R)) y))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) *)
apply Trans with (ring_mult x (monoid_unit R)); auto with algebra.
Qed.
End Lemmas.
Hint Resolve RING_assoc RING_comp RING_unit_r RING_unit_l RING_dist_r
  RING_dist_l RING_absorbant_r RING_absorbant_l RING_op_mult_l
  RING_op_mult_r: algebra.
Section Commutative_rings.
Variable R1 : CRING.

Lemma CRING_com : forall x y : R1, Equal (ring_mult x y) (ring_mult y x).
(* Goal: forall x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) x y) (@ring_mult (cring_ring R1) y x) *)
exact (cring_com_prf R1).
Qed.
Hint Immediate CRING_com: algebra.

Lemma CRING_mult4 :
 forall a b c d : R1,
 Equal (ring_mult (ring_mult a b) (ring_mult c d))
   (ring_mult (ring_mult a c) (ring_mult b d)).
(* Goal: forall a b c d : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) a b) (@ring_mult (cring_ring R1) c d)) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) a c) (@ring_mult (cring_ring R1) b d)) *)
intros a b c d; try assumption.
apply Trans with (ring_mult a (ring_mult b (ring_mult c d)));
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
apply Trans with (ring_mult a (ring_mult (ring_mult b c) d));
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
apply Trans with (ring_mult a (ring_mult (ring_mult c b) d));
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
apply Trans with (ring_mult a (ring_mult c (ring_mult b d)));
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
 auto with algebra.
Qed.
Hint Resolve CRING_mult4: algebra.

Lemma CRING_mult3 :
 forall x y z : R1,
 Equal (ring_mult x (ring_mult y z)) (ring_mult y (ring_mult x z)).
(* Goal: forall x y z : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x y) z) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x z) y) *)
intros x y z; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) x (@ring_mult (cring_ring R1) y z)) (@ring_mult (cring_ring R1) y (@ring_mult (cring_ring R1) x z)) *)
apply Trans with (ring_mult (ring_mult x y) z); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x y) z) (@ring_mult (cring_ring R1) y (@ring_mult (cring_ring R1) x z)) *)
apply Trans with (ring_mult (ring_mult y x) z); auto with algebra.
Qed.
Hint Resolve CRING_mult3: algebra.

Lemma CRING_mult3bis :
 forall x y z : R1,
 Equal (ring_mult (ring_mult x y) z) (ring_mult (ring_mult x z) y).
(* Goal: forall x y z : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x y) z) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x z) y) *)
intros x y z; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x y) z) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x z) y) *)
apply Trans with (ring_mult z (ring_mult x y)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) z (@ring_mult (cring_ring R1) x y)) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x z) y) *)
apply Trans with (ring_mult z (ring_mult y x)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) z (@ring_mult (cring_ring R1) y x)) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x z) y) *)
apply Trans with (ring_mult y (ring_mult z x)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring R1)))))) (@ring_mult (cring_ring R1) y (@ring_mult (cring_ring R1) z x)) (@ring_mult (cring_ring R1) (@ring_mult (cring_ring R1) x z) y) *)
apply Trans with (ring_mult (ring_mult z x) y); auto with algebra.
Qed.
Hint Resolve CRING_mult3bis: algebra.
End Commutative_rings.
Hint Resolve CRING_mult4 CRING_mult3 CRING_mult3bis: algebra.
Hint Immediate CRING_com: algebra.
Section Hom_lemmas.
Hint Resolve RING_comp: algebra.
Variable R R' : RING.
Variable f : Hom R R'.

Lemma RING_hom_prop :
 forall x y : R, Equal (f (ring_mult x y)) (ring_mult (f x) (f y)).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) (ring_unit R)) (ring_unit R') *)
case f; auto with algebra.
Qed.

Lemma RING_one_prop : Equal (f (ring_unit R)) (ring_unit R').
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) (ring_unit R)) (ring_unit R') *)
case f; auto with algebra.
Qed.

Lemma RING_hom_ext :
 forall f g : Hom R R', (forall x : R, Equal (f x) (g x)) -> Equal f g.
(* Goal: forall (f g : Carrier (@Hom RING R R')) (_ : forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' f))) x) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_sgroup (group_monoid (abelian_group_group (ring_group R')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (ring_group R))) (group_monoid (abelian_group_group (ring_group R'))) (@ring_plus_hom R R' g))) x)), @Equal (@Hom RING R R') f g *)
auto with algebra.
Qed.
End Hom_lemmas.
Hint Resolve RING_hom_prop RING_one_prop: algebra.