Require Import Pol_is_ring.
Require Import Ring_cat.
Require Import Ring_util.

Set Implicit Arguments.
Unset Strict Implicit.

Section POL.

Variable C:Type.
Variable Call:CALL C.

Lemma equiv_Pol1Eq:equivalence (Pol1Eq C (coef1 C Call)).
red in |- *.
split.
exact (Pol1Eq_refl C (coef1 C Call) (eq_th1 C Call)).
split.
red in |- *.
intros.
red in |- *.
apply (Pol1Eq_trans C (coef1 C Call) (eq_th1 C Call) x y H);auto.
red in |- *.
intros.
red in |- *.
apply (Pol1Eq_sym C (coef1 C Call) (eq_th1 C Call) x y H);auto.
Qed.


Definition POL1_setoid:Setoid.
apply (Build_Setoid (Carrier:=(Pol1 C)) (Equal:= (Pol1Eq C (coef1 C Call) )) equiv_Pol1Eq).
Defined.


Definition POL1:RING.
apply
 (BUILD_RING (E:=POL1_setoid) (ringplus:=Pol1_add C (coef1 C Call)) (ringmult:=Pol1_mul C (coef1 C Call)) (zero:=PO C (coef1 C Call))
    (un:=PI C (coef1 C Call)) (ringopp:=Pol1_opp C (coef1 C Call))).
intros.
apply (Pol1add_ext C (coef1 C Call)  (CT1 C Call) (eq_th1 C Call) x x' H y y' H0). 
intros;apply (Pol1Eq_sym C (coef1 C Call) (eq_th1 C Call) (Pol1_add C (coef1 C Call)  x (Pol1_add C (coef1 C Call) y z)) (Pol1_add C (coef1 C Call) (Pol1_add C (coef1 C Call)  x y) z));apply (Pol1add_assoc C (coef1 C Call)  (CT1 C Call) (eq_th1 C Call) x y z). 
intros;apply (Pol1add_0_l' C (coef1 C Call) (CT1 C Call) (eq_th1 C Call) x).
intros;apply (Pol1opp_ext C (coef1 C Call)  (CT1 C Call) (eq_th1 C Call) x y H).
intros;apply (Pol1opp_def C (coef1 C Call) (CT1 C Call) x).
intros;apply (Pol1add_sym C (coef1 C Call) (CT1 C Call) (eq_th1 C Call) x y).
intros;apply (Pol1mul_ext C (coef1 C Call)  (CT1 C Call) (eq_th1 C Call) x x' H y y' H0).
intros;apply (Pol1Eq_sym C  (coef1 C Call) (eq_th1 C Call) (Pol1_mul C (coef1 C Call) x (Pol1_mul C (coef1 C Call) y z)) (Pol1_mul C (coef1 C Call) (Pol1_mul C (coef1 C Call) x y) z));apply (Pol1mul_assoc C (coef1 C Call) (CT1 C Call) (eq_th1 C Call) x y z).
intros;apply (Pol1mul_1_r C (coef1 C Call) (CT1 C Call) (eq_th1 C Call) x).
intros;apply (Pol1mul_1_l C (coef1 C Call) (CT1 C Call) (eq_th1 C Call)  x).
intros;apply (Pol1distr_r C (coef1 C Call) (CT1 C Call) (eq_th1 C Call) x y z).
intros;apply (Pol1distr_l C (coef1 C Call) (CT1 C Call) (eq_th1 C Call) z x y).
Defined.



Variable n:nat.


Lemma equiv_PolnEq:equivalence (PolnEq C Call n ).
red in |- *.
split.
exact (PolnEq_refl C Call n).
split.
red in |- *.
intros.
red in |- *.
apply (PolnEq_trans C Call n x y );auto.
red in |- *.
intros.
red in |- *.
apply (PolnEq_sym C Call n x y H);auto.
Qed.

Definition POLn_setoid:Setoid.
apply (Build_Setoid (Carrier:=(Pol C n)) (Equal:= (PolnEq C Call  n)) equiv_PolnEq).
Defined.

Definition POLn:RING.
apply
 (BUILD_RING (E:=POLn_setoid) (ringplus:=Poln_add C Call n) (ringmult:=Poln_mul C Call n) (zero:=P0 C Call n)
    (un:=P1 C Call n) (ringopp:=Poln_opp C Call n)).
intros.
apply (Polnadd_ext C Call n x x' H y y' H0). 
intros;apply (PolnEq_sym C  Call n (Poln_add C Call n x  (Poln_add C Call n y z)) (Poln_add C Call  n (Poln_add C Call n x y) z));apply (Polnadd_assoc C Call n x y z). 
intros;apply (Polnadd_0_r C Call n x).
intros;apply (Polnopp_ext C Call n x y H).
intros;apply (Polnopp_def C Call n x).
intros;apply (Polnadd_sym C Call n x y).
intros;apply (Polnmul_ext C Call n x x' H y y' H0).
intros;apply (PolnEq_sym C  Call n (Poln_mul C Call n x (Poln_mul C Call n y z)) (Poln_mul C Call n (Poln_mul C Call n x y) z));apply (Polnmul_assoc C Call n x y z).
intros;apply (Polnmul_1_r C Call n x).
intros;apply (Polnmul_1_l C Call n x).
intros;apply (Polndistr_r C Call n x y z).
intros;apply (Polndistr_l C Call n z x y).
Defined.


End POL.