(* 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 ZArith.
Require Export ZArith.
Require Export auxiliary.
Require Export ZArith_dec.
Require Export Zmisc.
Hint Resolve Zle_refl: algebra.
Require Export Ring_util.
Require Export Integral_domain_facts.

Definition Zr_aux : RING.
apply
 (BUILD_RING (E:=Leibnitz_set BinInt.Z) (ringplus:=Zplus) (ringmult:=Zmult)
    (zero:=0%Z) (un:=1%Z) (ringopp:=Zopp)).
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall (x x' y y' : Z) (_ : @eq Z x x') (_ : @eq Z y y'), @eq Z (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
intros x x' y y' H' H'0; try assumption.
(* Goal: @eq Z x Z0 *)
rewrite H'0.
(* Goal: @eq Z y Z0 *)
rewrite H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
intros x y z; try assumption.
(* Goal: @Equal (Leibnitz_set Z) (Z.add (Z.add x y) z) (Z.add x (Z.add y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x Z0) x *)
(* Goal: forall (x y : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x y), @Equal (Leibnitz_set Z) (Z.opp x) (Z.opp y) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x (Z.opp x)) Z0 *)
(* Goal: forall x y : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x y) (Z.add y x) *)
(* Goal: forall (x x' y y' : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x x') (_ : @Equal (Leibnitz_set Z) y y'), @Equal (Leibnitz_set Z) (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
apply Sym.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: @eq Z (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x Z0) x *)
(* Goal: forall (x y : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x y), @Equal (Leibnitz_set Z) (Z.opp x) (Z.opp y) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x (Z.opp x)) Z0 *)
(* Goal: forall x y : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x y) (Z.add y x) *)
(* Goal: forall (x x' y y' : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x x') (_ : @Equal (Leibnitz_set Z) y y'), @Equal (Leibnitz_set Z) (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zplus_assoc.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @eq Z (Z.add x (Z.add y z)) (Z.add (Z.add x y) z) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x Z0) x *)
(* Goal: forall (x y : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x y), @Equal (Leibnitz_set Z) (Z.opp x) (Z.opp y) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x (Z.opp x)) Z0 *)
(* Goal: forall x y : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x y) (Z.add y x) *)
(* Goal: forall (x x' y y' : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x x') (_ : @Equal (Leibnitz_set Z) y y'), @Equal (Leibnitz_set Z) (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
rewrite (H' x y z).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall x : Z, sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros x; try assumption.
(* Goal: @eq Z (Z.add x Z0) x *)
(* Goal: forall (x y : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x y), @Equal (Leibnitz_set Z) (Z.opp x) (Z.opp y) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x (Z.opp x)) Z0 *)
(* Goal: forall x y : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x y) (Z.add y x) *)
(* Goal: forall (x x' y y' : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x x') (_ : @Equal (Leibnitz_set Z) y y'), @Equal (Leibnitz_set Z) (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zplus_0_r.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x); auto with algebra.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall (x y : Z) (_ : @eq Z x y), @eq Z (Z.opp x) (Z.opp y) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x (Z.opp x)) Z0 *)
(* Goal: forall x y : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x y) (Z.add y x) *)
(* Goal: forall (x x' y y' : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x x') (_ : @Equal (Leibnitz_set Z) y y'), @Equal (Leibnitz_set Z) (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
intros x y H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite H'; auto with algebra.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall x : Z, sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros x; try assumption.
(* Goal: @eq Z (Z.add x (Z.opp x)) Z0 *)
(* Goal: forall x y : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.add x y) (Z.add y x) *)
(* Goal: forall (x x' y y' : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x x') (_ : @Equal (Leibnitz_set Z) y y'), @Equal (Leibnitz_set Z) (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zplus_opp_r.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x); auto with algebra.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
intros x y; try assumption.
(* Goal: @eq Z (Z.add x y) (Z.add y x) *)
(* Goal: forall (x x' y y' : Carrier (Leibnitz_set Z)) (_ : @Equal (Leibnitz_set Z) x x') (_ : @Equal (Leibnitz_set Z) y y'), @Equal (Leibnitz_set Z) (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zplus_comm.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x y); auto with algebra.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall (x x' y y' : Z) (_ : @eq Z x x') (_ : @eq Z y y'), @eq Z (Z.mul x y) (Z.mul x' y') *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
intros x x' y y' H' H'0; try assumption.
(* Goal: @eq Z x Z0 *)
rewrite H'0.
(* Goal: @eq Z y Z0 *)
rewrite H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
intros x y z; try assumption.
(* Goal: @eq Z (Z.mul (Z.mul x y) z) (Z.mul x (Z.mul y z)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zmult_assoc.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x y z); auto with algebra.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall x : Z, sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros x; try assumption.
(* Goal: @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zmult_1_l.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @eq Z (Z.mul x (Zpos xH)) x *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
replace (x * 1)%Z with (1 * x)%Z.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x); auto with algebra.
(* Goal: @eq Z (Z.mul (Zpos xH) x) (Z.mul x (Zpos xH)) *)
(* Goal: forall x : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
apply BinInt.Zmult_comm.
(* Goal: forall x : Z, sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros x; try assumption.
(* Goal: @Equal (Leibnitz_set Z) (Z.mul (Zpos xH) x) x *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zmult_1_l.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x); auto with algebra.
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
intros x y z; try assumption.
(* Goal: @Equal (Leibnitz_set Z) (Z.mul x (Z.add y z)) (Z.add (Z.mul x y) (Z.mul x z)) *)
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zmult_plus_distr_r.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x y z); auto with algebra.
(* Goal: forall x y z : Carrier (Leibnitz_set Z), @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
intros x y z; try assumption.
(* Goal: @Equal (Leibnitz_set Z) (Z.mul (Z.add x y) z) (Z.add (Z.mul x z) (Z.mul y z)) *)
generalize BinInt.Zmult_plus_distr_l.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x y z); auto with algebra.
Defined.

Definition Zr : CRING.
(* Goal: Ob CRING *)
apply (Build_cring (cring_ring:=Zr_aux)).
(* Goal: cring_on Zr_aux *)
apply (Build_cring_on (R:=Zr_aux)).
(* Goal: idomain_prop Zr *)
red in |- *.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
intros x y; try assumption.
(* Goal: @eq Z (Z.mul x y) (Z.mul y x) *)
generalize BinInt.Zmult_comm.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
rewrite (H' x y); auto with algebra.
Defined.

Definition Zzero_dec :
  forall x : Zr, {Equal x (monoid_unit Zr)} + {~ Equal x (monoid_unit Zr)}.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall x : Z, sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros x; try assumption.
(* Goal: sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
case (Z_eq_dec x 0).
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
cut (x = 0%Z :>BinInt.Z).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: @eq Z y Z0 *)
rewrite H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: forall _ : not (@eq Z x Z0), sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
intros H'; try assumption.
(* Goal: sumbool (@eq Z x Z0) (not (@eq Z x Z0)) *)
cut (x <> 0%Z :>BinInt.Z).
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: idomain_prop Zr *)
red in |- *.
(* Goal: forall _ : @eq Z x Z0, False *)
intros H'0; try assumption.
(* Goal: False *)
apply H'.
(* Goal: @eq Z x Z0 *)
rewrite H'0.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
Defined.

Definition ZZ : INTEGRAL_DOMAIN.
(* Goal: Ob INTEGRAL_DOMAIN *)
apply (Build_idomain (idomain_ring:=Zr)).
(* Goal: idomain_on Zr *)
apply Build_idomain_on.
(* Goal: idomain_prop Zr *)
red in |- *.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
intros x y; try assumption.
(* Goal: forall (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))) (_ : not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) y (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))))), not (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) x y) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))) (monoid_on_def (group_monoid (abelian_group_group (ring_group (cring_ring Zr))))))) *)
simpl in |- *.
(* Goal: forall (_ : not (@eq Z x Z0)) (_ : not (@eq Z y Z0)), not (@eq Z (@ring_mult Zr_aux x y) Z0) *)
generalize (BinInt.Zmult_integral_l x y).
(* Goal: forall (_ : forall (_ : not (@eq Z x Z0)) (_ : @eq Z (Z.mul y x) Z0), @eq Z y Z0) (_ : not (@eq Z x Z0)) (_ : not (@eq Z y Z0)), not (@eq Z (@ring_mult Zr_aux x y) Z0) *)
unfold not in |- *.
(* Goal: forall (_ : forall (_ : forall _ : @eq Z x Z0, False) (_ : @eq Z (Z.mul y x) Z0), @eq Z y Z0) (_ : forall _ : @eq Z x Z0, False) (_ : forall _ : @eq Z y Z0, False) (_ : @eq Z (@ring_mult Zr_aux x y) Z0), False *)
intros H' H'0 H'1 H'2; try assumption.
(* Goal: False *)
apply H'1.
(* Goal: @eq Z y Z0 *)
rewrite H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: forall _ : @eq Z x Z0, False *)
(* Goal: @eq Z (Z.mul y x) Z0 *)
intros H'3; try assumption.
(* Goal: False *)
(* Goal: @eq Z (Z.mul y x) Z0 *)
apply H'0.
(* Goal: @eq Z x Z0 *)
(* Goal: @eq Z (Z.mul y x) Z0 *)
rewrite H'3.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
(* Goal: @eq Z (Z.mul y x) Z0 *)
rewrite <- H'2.
(* Goal: @eq Z (Z.mul y x) (@ring_mult Zr_aux x y) *)
change (Equal (ring_mult y x) (ring_mult x y)) in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group (cring_ring Zr)))))) (@ring_mult (cring_ring Zr) y x) (@ring_mult (cring_ring Zr) x y) *)
auto with algebra.
Defined.
