# Library Coq.ring.LegacyRing_theory

Require Export Bool.
Section Theory_of_semi_rings.
Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aeq : A -> A -> bool.
Infix "+" := Aplus (at level 50, left associativity).
Infix "*" := Amult (at level 40, left associativity).
Notation "0" := Azero.
Notation "1" := Aone.
Record Semi_Ring_Theory : Prop :=
{SR_plus_comm : forall n m:A, n + m = m + n;
SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
SR_mult_comm : forall n m:A, n * m = m * n;
SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
SR_plus_zero_left : forall n:A, 0 + n = n;
SR_mult_one_left : forall n:A, 1 * n = n;
SR_mult_zero_left : forall n:A, 0 * n = 0;
SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
Variable T : Semi_Ring_Theory.
Let plus_comm := SR_plus_comm T.
Let plus_assoc := SR_plus_assoc T.
Let mult_comm := SR_mult_comm T.
Let mult_assoc := SR_mult_assoc T.
Let plus_zero_left := SR_plus_zero_left T.
Let mult_one_left := SR_mult_one_left T.
Let mult_zero_left := SR_mult_zero_left T.
Let distr_left := SR_distr_left T.
Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
mult_one_left mult_zero_left distr_left .
Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p).
Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n.
Lemma SR_mult_one_left2 : forall n:A, n = 1 * n.
Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n.
Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p).
Hint Resolve SR_plus_permute SR_mult_permute.
Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
Lemma SR_mult_zero_right : forall n:A, n * 0 = 0.
Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0.
Lemma SR_plus_zero_right : forall n:A, n + 0 = n.
Lemma SR_plus_zero_right2 : forall n:A, n = n + 0.
Lemma SR_mult_one_right : forall n:A, n * 1 = n.
Lemma SR_mult_one_right2 : forall n:A, n = n * 1.
End Theory_of_semi_rings.
Section Theory_of_rings.
Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aopp : A -> A.
Variable Aeq : A -> A -> bool.
Infix "+" := Aplus (at level 50, left associativity).
Infix "*" := Amult (at level 40, left associativity).
Notation "0" := Azero.
Notation "1" := Aone.
Notation "- x" := (Aopp x).
Record Ring_Theory : Prop :=
{Th_plus_comm : forall n m:A, n + m = m + n;
Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
Th_mult_comm : forall n m:A, n * m = m * n;
Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
Th_plus_zero_left : forall n:A, 0 + n = n;
Th_mult_one_left : forall n:A, 1 * n = n;
Th_opp_def : forall n:A, n + - n = 0;
Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
Variable T : Ring_Theory.
Let plus_comm := Th_plus_comm T.
Let plus_assoc := Th_plus_assoc T.
Let mult_comm := Th_mult_comm T.
Let mult_assoc := Th_mult_assoc T.
Let plus_zero_left := Th_plus_zero_left T.
Let mult_one_left := Th_mult_one_left T.
Let opp_def := Th_opp_def T.
Let distr_left := Th_distr_left T.
Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
mult_one_left opp_def distr_left.
Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p).
Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n.
Lemma Th_mult_one_left2 : forall n:A, n = 1 * n.
Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
Lemma Th_opp_def2 : forall n:A, 0 = n + - n.
Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p).
Hint Resolve Th_plus_permute Th_mult_permute.
Lemma aux1 : forall a:A, a + a = a -> a = 0.
Lemma Th_mult_zero_left : forall n:A, 0 * n = 0.
Hint Resolve Th_mult_zero_left.
Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n.
Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z.
Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y.
Hint Resolve Th_opp_mult_left.
Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y).
Lemma Th_mult_zero_right : forall n:A, n * 0 = 0.
Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0.
Lemma Th_plus_zero_right : forall n:A, n + 0 = n.
Lemma Th_plus_zero_right2 : forall n:A, n = n + 0.
Lemma Th_mult_one_right : forall n:A, n * 1 = n.
Lemma Th_mult_one_right2 : forall n:A, n = n * 1.
Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y.
Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y).
Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y).
Lemma Th_plus_permute_opp : forall n m p:A, - m + (n + p) = n + (- m + p).
Lemma Th_opp_opp : forall n:A, - - n = n.
Hint Resolve Th_opp_opp.
Lemma Th_opp_opp2 : forall n:A, n = - - n.
Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y.
Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y.
Lemma Th_opp_zero : - 0 = 0.
Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
End Theory_of_rings.
Hint Resolve Th_mult_zero_left : core.
Definition Semi_Ring_Theory_of :
forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A)
(Aopp:A -> A) (Aeq:A -> A -> bool),
Ring_Theory Aplus Amult Aone Azero Aopp Aeq ->
Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
Defined.
Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory.
Section product_ring.
End product_ring.
Section power_ring.
End power_ring.