Library noetred_tes
Require Export Axiomas_n_full2_tes.
Definition inc_red: pol_full -> pol_full -> pol_full -> Prop :=
[p,q,r:pol_full] (red (inc p) (inc q) (inc r)).
Lemma aux1_red_menor2: (a:Q)(b,t:term)(p,x:pol)(full_pol (cpol (a,b) p))->
(term_in_pol (cpol (a,b) p) t)->~(equpol x vpol)->(full_term_pol x)->
(equpol (cpol (a,b) p)
(suma_app x (cpol ((coef (cpol (a,b) p) t),t) vpol)))->
((t':term)(term_in_pol x t')->(Ttm t t'))->(term_in_pol p t).
Intros.
Elim (eq_tm_dec t b); Intros.
Rewrite <- a0 in H.
Rewrite <- a0 in H0.
Cut (hterm (cpol (a,t) p))=t; Intros.
Cut (Ttm t (hterm (cpol (a,t) p))); Intros.
Rewrite H5 in H6.
Cut ~(Ttm t t); Intros; Auto.
Elim H7; Auto.
Rewrite <- a0 in H3.
Replace (hterm (cpol (a,t) p))
with (hterm (suma_app x (cpol ((coef (cpol (a,t) p) t),t) vpol))).
Replace (hterm (suma_app x (cpol ((coef (cpol (a,t) p) t),t) vpol)))
with (hterm x); Auto.
Symmetry.
Apply hterm_suma_Ttm; Auto.
Apply full_term_pol_cons; Auto.
Inversion H; Auto.
Replace (hterm (cpol ((coef (cpol (a,t) p) t),t) vpol)) with t; Auto.
Symmetry.
Apply full_hterm.
Apply full_pol_cons; Auto.
Inversion H; Auto.
Apply eq_hterm; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_pol_cons; Auto.
Inversion H; Auto.
Apply full_hterm; Auto.
Red.
Red; Intros.
Red in H0.
Apply H0.
Apply eqQ_trans with (coef p t); Trivial.
Apply coef_n_term; Trivial.
Save.
Lemma aux2_red_menor2: (a:Q)(b,t:term)(p,x,x0:pol)(full_pol (cpol (a,b) p))->
(term_in_pol (cpol (a,b) p) t)->~(equpol x vpol)->~(equpol x0 vpol)->
(full_term_pol x)->(full_term_pol x0)->
(equpol (cpol (a,b) p)
(suma_app x
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0)))->
((t':term)(term_in_pol x t')->(Ttm t t'))->((t':term)(term_in_pol x0 t')->(Ttm t' t))->(term_in_pol p t).
Intros.
Elim (eq_tm_dec t b); Intros.
Rewrite <- a0 in H.
Rewrite <- a0 in H0.
Cut (hterm (cpol (a,t) p))=t; Intros; Auto.
Cut (Ttm t (hterm (cpol (a,t) p))); Intros.
Rewrite H8 in H9.
Cut ~(Ttm t t); Intros; Auto.
Elim H10; Auto.
Rewrite <- a0 in H5.
Replace (hterm (cpol (a,t) p))
with (hterm
(suma_app x
(suma_app (cpol ((coef (cpol (a,t) p) t),t) vpol) x0))).
Replace (hterm
(suma_app x
(suma_app (cpol ((coef (cpol (a,t) p) t),t) vpol) x0)))
with (hterm x); Auto.
Symmetry.
Apply hterm_suma_Ttm; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_pol_cons; Auto.
Inversion H; Auto.
Replace (hterm (suma_app (cpol ((coef (cpol (a,t) p) t),t) vpol) x0))
with t; Auto.
Symmetry.
Transitivity (hterm (cpol ((coef (cpol (a,t) p) t),t) vpol)).
Apply hterm_suma_Ttm; Auto.
Apply full_term_pol_cons; Auto.
Inversion H; Auto.
Replace (hterm (cpol ((coef (cpol (a,t) p) t),t) vpol)) with t; Auto.
Symmetry.
Apply full_hterm.
Apply full_pol_cons; Auto.
Inversion H; Auto.
Apply full_hterm.
Apply full_pol_cons; Auto.
Inversion H; Auto.
Apply eq_hterm; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_pol_cons; Auto.
Inversion H; Auto.
Red.
Red; Intros.
Red in H0.
Apply H0.
Apply eqQ_trans with (coef p t); Auto.
Save.
Lemma red_menor2: (f,g,fi:pol_full)(inc_red fi f g)->(Tpol_full g f).
Unfold inc_red.
Unfold Tpol_full.
Induction f; Simpl; Clear f.
Intros f ff.
Induction g; Simpl; Clear g.
Intros g fg.
Induction fi; Simpl; Clear fi.
Intros fi ffi.
Generalize f ff g fg fi ffi; Clear ffi fi fg g ff f.
Induction f.
Intros.
Inversion H.
Elim H0.
Simpl; Trivial.
Induction m.
Induction g.
Intros.
Apply Tpol_Lex3_v.
Inversion ff; Auto.
Inversion ff; Auto.
Induction m0; Intros.
Inversion H1; Inversion ff; Inversion fg.
Cut (full_term_pol p); Auto; Intros.
Cut (full_term_pol p0); Auto; Intros.
Elim (vpol_dec_full_term (cpol (a0,b0) p0)); Trivial; Intros.
Cut (cpol (a0,b0) p0)=vpol; Intros.
Rewrite H25; Auto.
Apply full_eq_vpol; Trivial.
Cut (no_term_in_pol (cpol (a0,b0) p0) t); Intros.
Cut (hterm
(pol_opp
(mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))=t; Intros.
Elim split_pol with (cpol (a,b) p) t; Trivial; Intros.
Elim H28; Intros; Clear H28.
Elim H27; Intros; Clear H27.
Elim H29; Intros; Clear H29.
Cut (full n t); Intros.
Cut ~(equpol (cpol (a,b) p) vpol); Intros.
Cut (eqQ (hcoef (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi))))))
(multQ_neg (coef (cpol (a,b) p) t))); Intros.
Cut (full_pol (cpol ((coef (cpol (a,b) p) t),t) vpol)); Intros.
Cut (full_term_pol (suma_app x (cpol ((coef (cpol (a,b) p) t),t) vpol)));
Intros.
Cut (full_term_pol
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0)); Intros.
Cut ~(z_monom
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi)))).
Cut ~(equpol (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi))))) vpol);
Intros.
Cut (full_term_pol (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))); Intros.
Cut (full_mon n ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))); Intros.
Elim (vpol_dec_full_term x); Trivial; Intros.
Elim (vpol_dec_full_term x0); Trivial; Intros.
Cut (equpol (cpol (a,b) p) (cpol ((coef (cpol (a,b) p) t),t) vpol)); Intros.
Apply Tpol_Lex3_car; Simpl; Auto.
Replace b0 with (hterm (cpol (a0,b0) p0)); Auto.
Replace b with (hterm (cpol (a,b) p)); Auto.
Replace (hterm (cpol (a0,b0) p0)) with (hterm (suma_app (cpol (a,b) p)
(pol_opp (mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Replace (hterm (suma_app (cpol (a,b) p) (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi)))))))
with (hterm (suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol)
(pol_opp (mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Replace (hterm (cpol (a,b) p))
with (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)); Auto.
Apply hterm_eq_suma_Ttm; Auto.
Apply eq_nvpol with (cpol (a0,b0) p0); Trivial.
Apply equpol_tran with (suma_app (cpol (a,b) p)
(pol_opp (mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))); Trivial.
Apply equpol_ss; Auto.
Apply eqQ_trans with (coef (cpol (a,b) p) t).
Apply full_hcoef; Auto.
Apply eqQ_trans with (hcoef (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi))))).
Apply eqQ_trans with (multQ (hcoef fi) (mon_coef
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi))))).
Unfold mon_coef.
Apply eqQ_sym.
Apply eqQ_trans with (multQ (divQ (coef (cpol (a,b) p) t) (hcoef fi))
(hcoef fi)); Auto.
Apply eqQ_trans with (divQ (multQ (coef (cpol (a,b) p) t) (hcoef fi))
(hcoef fi)); Auto.
Apply eqQ_trans with (divQ (multQ (hcoef fi) (coef (cpol (a,b) p) t))
(hcoef fi)); Auto.
Apply eqQ_sym.
Apply hcoef_mult; Trivial.
Apply hcoef_pol_opp_term; Auto.
Transitivity t.
Apply full_hterm; Auto.
Symmetry; Auto.
Apply equpol_tran with (suma_app x (suma_app
(cpol ((coef (cpol (a,b) p) t),t) vpol) x0)); Auto.
Apply equpol_tran with (suma_app vpol
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) vpol)); Auto.
Cut (equpol (cpol (a,b) p)
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0)); Intros.
Cut (hterm (cpol (a,b) p))=t; Intros.
Cut (eqQ (hcoef (cpol (a,b) p))
(hcoef (cpol ((coef (cpol (a,b) p) t),t) vpol))); Intros.
Cut (equpol (cpol (a0,b0) p0) (suma_app
(cpol ((coef (cpol (a,b) p) t),t) vpol)
(suma_app x0 (pol_opp (mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))))); Intros.
Cut (hterm (cpol (a,b) p))
=(hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)); Intros.
Apply Tpol_Lex3_car; Simpl; Auto.
Replace b0 with (hterm (cpol (a0,b0) p0)); Auto.
Replace b with (hterm (cpol (a,b) p)); Auto.
Replace (hterm (cpol (a0,b0) p0)) with (hterm
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol)
(suma_app x0 (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))))); Auto.
Rewrite H46.
Apply hterm_eq_suma_Ttm; Auto.
Apply eq_nvpol with (cpol (a0,b0) p0); Trivial.
Apply eqQ_trans with (multQ_neg (hcoef (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi))))))).
Apply eqQ_trans with (hcoef (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi))))); Auto.
Apply eqQ_trans with (multQ (hcoef fi) (mon_coef
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),(div_term t (hterm fi))))).
Unfold mon_coef.
Apply eqQ_trans with (coef (cpol (a,b) p) t); Auto.
Apply eqQ_sym.
Apply eqQ_trans with
(multQ (divQ (coef (cpol (a,b) p) t) (hcoef fi)) (hcoef fi)); Auto.
Apply eqQ_trans with
(divQ (multQ (coef (cpol (a,b) p) t) (hcoef fi)) (hcoef fi)); Auto.
Apply eqQ_trans with
(divQ (multQ (hcoef fi) (coef (cpol (a,b) p) t)) (hcoef fi)); Auto.
Apply eqQ_sym.
Apply hcoef_mult; Trivial.
Apply eq_mulQ_neg.
Apply eqQ_trans with (hcoef (suma_app (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))) x0)); Auto.
Apply hcoef_suma_Ttm; Trivial.
Rewrite H26; Apply H32; Auto.
Symmetry.
Transitivity (hterm (suma_app (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))) x0)); Auto.
Transitivity (hterm (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))).
Apply hterm_suma_Ttm; Auto.
Rewrite H26; Apply H32; Auto.
Transitivity t; Trivial.
Symmetry; Auto.
Transitivity t; Trivial.
Symmetry; Apply full_hterm; Auto.
Apply equpol_tran with (suma_app (cpol (a,b) p) (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))); Auto.
Apply equpol_tran with (suma_app (suma_app
(cpol ((coef (cpol (a,b) p) t),t) vpol) x0) (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))); Auto.
Apply eqQ_trans with (coef (cpol (a,b) p) (hterm (cpol (a,b) p))); Auto.
Apply eqQ_sym.
Apply eqQ_trans with (coef (cpol ((coef (cpol (a,b) p) t),t) vpol)
(hterm (cpol ((coef (cpol (a,b) p) t),t) vpol))); Auto.
Rewrite H43.
Replace (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)) with t.
Simpl.
Elim (eq_tm_dec t t).
Intros.
Elim (eq_tm_dec t b); Intros; Auto.
Intro e; Elim e; Auto.
Symmetry; Auto.
Transitivity (hterm (suma_app
(cpol ((coef (cpol (a,b) p) t),t) vpol) x0)); Auto.
Transitivity (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)); Auto.
Apply hterm_suma_Ttm; Auto.
Replace (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)) with t; Auto.
Symmetry.
Apply full_hterm; Auto.
Apply equpol_tran with (suma_app x
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0)); Trivial.
Apply equpol_tran with (suma_app vpol
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0)); Auto.
(Elim (vpol_dec_full_term x0); Trivial; Intros).
Cut (equpol (cpol (a,b) p)
(suma_app x (cpol ((coef (cpol (a,b) p) t),t) vpol))); Intros.
Cut b0=b; Intros.
Rewrite <- H43.
Apply Tpol_Lex3_cdr; Auto.
Apply H with fi; Auto.
Apply red1_simpl with t; Auto.
Apply aux1_red_menor2 with a b x; Auto.
Apply eq_cpol with (a,b).
Apply equpol_tran with (cpol (a0,b0) p0).
Apply eq_mon_cpol.
Rewrite H43.
Red.
Right.
Split; Auto.
Apply eqQ_trans with (hcoef (cpol (a,b) p)); Auto.
Apply eqQ_trans with (hcoef (cpol (a0,b0) p0)); Auto.
Apply eqQ_trans with (hcoef (suma_app (cpol (a,b) p)
(pol_opp (mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Apply eqQ_sym.
Apply hcoef_suma_Ttm; Auto.
Rewrite H26.
Replace (hterm (cpol (a,b) p)) with
(hterm (suma_app x (cpol ((coef (cpol (a,b) p) t),t) vpol))); Auto.
Replace (hterm (suma_app x (cpol ((coef (cpol (a,b) p) t),t) vpol)))
with (hterm x); Auto.
Symmetry.
Apply hterm_suma_Ttm; Auto.
Replace (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)) with t; Auto.
Symmetry.
Apply term_monom_hterm; Auto.
Apply equpol_tran with (suma_app (cpol (a,b) p)
(pol_opp (mult_m fi((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))); Auto.
Apply equpol_tran with (cpol (a,b) (suma_app p (pol_opp
(mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Apply equpol_cpol.
Apply monot_suma_l.
Apply opp_comp.
Apply mult_pm_comp_2.
Red.
Right.
Split; Auto.
Apply eg_denomQ; Auto.
Cut (term_in_pol p t); Intros; Simpl.
Elim (eq_tm_dec t b); Intros; Auto.
Rewrite <- a4 in ff.
Cut (no_term_in_pol p t); Intros.
Red in H44.
Red in H45.
Elim H44; Auto.
Apply full_no_term with a; Auto.
Apply aux1_red_menor2 with a b x; Auto.
Transitivity (hterm (cpol (a,b) p)); Auto.
Transitivity (hterm (cpol (a0,b0) p0)).
Symmetry; Auto.
Transitivity (hterm (suma_app (cpol (a,b) p) (pol_opp (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Apply hterm_suma_Ttm; Auto.
Rewrite H26.
Replace (hterm (cpol (a,b) p)) with b.
Apply H31.
Cut (term_in_pol p t); Intros.
Cut ~b=t; Intros.
Cut (term_in_pol (suma_app x (cpol ((coef (cpol (a,b) p) t),t) vpol)) b);
Intros.
Elim (term_in_sum x (cpol ((coef (cpol (a,b) p) t),t) vpol) b); Intros;
Auto.
Cut b=t; Intros.
Elim H44; Auto.
Apply eq_term_in_pol_monom with (coef (cpol (a,b) p) t); Auto.
Apply comp_term_in_pol with (cpol (a,b) p); Auto.
Replace b with (hterm (cpol (a,b) p)); Auto.
Replace (cpol (a,(hterm (cpol (a,b) p))) p) with (cpol (a,b) p); Auto.
Replace (hterm (cpol (a,b) p)) with b; Auto.
Symmetry; Auto.
Red; Intros.
Rewrite <- H44 in H43.
Cut (no_term_in_pol p b); Intros; Auto.
Apply full_no_term with a; Auto.
Apply aux1_red_menor2 with a b x; Auto.
Symmetry; Auto.
Apply equpol_tran with
(suma_app x (suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0)); Auto.
Apply equpol_tran with (suma_app x
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) vpol)); Auto.
Cut b0=b; Intros.
Rewrite <- H42.
Apply Tpol_Lex3_cdr; Auto.
Apply H with fi; Auto.
Apply red1_simpl with t; Auto.
Apply aux2_red_menor2 with a b x x0; Auto.
Apply eq_cpol with (a,b).
Apply equpol_tran with (cpol (a0,b0) p0).
Apply eq_mon_cpol.
Rewrite H42.
Red.
Right.
Split; Auto.
Apply eqQ_trans with (hcoef (cpol (a,b) p)); Auto.
Apply eqQ_trans with (hcoef (cpol (a0,b0) p0)); Auto.
Apply eqQ_trans with (hcoef (suma_app (cpol (a,b) p)
(pol_opp (mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Apply eqQ_sym.
Apply hcoef_suma_Ttm; Auto.
Rewrite H26.
Replace (hterm (cpol (a,b) p)) with (hterm (suma_app x
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0))); Auto.
Replace (hterm (suma_app x (suma_app
(cpol ((coef (cpol (a,b) p) t),t) vpol) x0))) with (hterm x); Auto.
Symmetry.
Apply hterm_suma_Ttm; Auto.
Replace (hterm (suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0))
with t; Auto.
Symmetry.
Transitivity (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)); Auto.
Apply hterm_suma_Ttm; Auto.
Replace (hterm (suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0))
with t.
Replace (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)) with t; Auto.
Symmetry.
Apply term_monom_hterm; Auto.
Symmetry.
Transitivity (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)); Auto.
Apply hterm_suma_Ttm; Auto.
Replace (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)) with t; Auto.
Symmetry.
Apply term_monom_hterm; Auto.
Apply equpol_tran with (suma_app (cpol (a,b) p) (pol_opp
(mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))); Auto.
Apply equpol_tran with (cpol (a,b) (suma_app p (pol_opp
(mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Apply equpol_cpol.
Apply monot_suma_l.
Apply opp_comp.
Apply mult_pm_comp_2.
Red.
Right.
Split; Auto.
Apply eg_denomQ; Auto.
Cut (term_in_pol p t); Intros.
Simpl.
Elim (eq_tm_dec t b); Intros; Auto.
Rewrite <- a3 in ff.
Cut (no_term_in_pol p t); Intros.
Red in H43.
Red in H44.
Elim H43; Auto.
Apply full_no_term with a; Auto.
Apply aux2_red_menor2 with a b x x0; Auto.
Transitivity (hterm (cpol (a,b) p)); Auto.
Transitivity (hterm (cpol (a0,b0) p0)); Auto.
Symmetry; Auto.
Transitivity (hterm (suma_app (cpol (a,b) p) (pol_opp
(mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Apply hterm_suma_Ttm; Auto.
Rewrite H26.
Replace (hterm (cpol (a,b) p)) with (hterm (suma_app x
(suma_app (cpol ((coef (cpol (a,b) p) t),t) vpol) x0))); Intros.
Replace (hterm (suma_app x (suma_app
(cpol ((coef (cpol (a,b) p) t),t) vpol) x0))) with (hterm x); Intros.
Apply H31; Auto.
Symmetry.
Apply hterm_suma_Ttm; Auto.
Apply Ttm_suma_hterm; Auto.
Replace (hterm (cpol ((coef (cpol (a,b) p) t),t) vpol)) with t; Auto.
Symmetry.
Apply term_monom_hterm; Auto.
Apply Ttm_trans with t n; Auto.
Auto.
Auto.
Auto.
Apply no_eq_no_vpol_opp.
Apply contr_mult_nz_monom; Auto.
Apply no_divQ_zero; Auto.
Unfold z_monom.
Apply no_divQ_zero; Auto.
Auto.
Auto.
Auto.
Apply eqQ_trans with (multQ_neg (hcoef (pol_opp (pol_opp
(mult_m fi ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi)))))))).
Apply hcoef_pol_opp_term; Auto.
Apply eq_mulQ_neg.
Apply eqQ_trans with (hcoef (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))).
Apply eqQ_trans with (multQ (hcoef fi)
(mon_coef ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))).
Unfold mon_coef.
Apply eqQ_sym.
Apply eqQ_trans with
(multQ (divQ (coef (cpol (a,b) p) t) (hcoef fi)) (hcoef fi)); Auto.
Apply eqQ_trans with
(divQ (multQ (coef (cpol (a,b) p) t) (hcoef fi)) (hcoef fi)); Auto.
Apply eqQ_trans with
(divQ (multQ (hcoef fi) (coef (cpol (a,b) p) t)) (hcoef fi)); Auto.
Apply eqQ_sym.
Apply hcoef_mult; Trivial.
Simpl; Auto.
Apply eq_hcoef; Auto.
Apply full_term_opp; Auto.
EAuto.
Apply full_coef with (cpol (a,b) p); Trivial.
Transitivity (hterm (mult_m fi
((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))).
Symmetry.
Apply hterm_pol_opp_term.
Apply full_mult_m; Auto.
Apply term_div_full; Auto.
Apply full_coef with (cpol (a,b) p); Trivial.
Transitivity (term_mult (hterm fi)
(mon_term ((divQ (coef (cpol (a,b) p) t) (hcoef fi)),
(div_term t (hterm fi))))).
Apply hterm_mult_m; Trivial.
Simpl.
Apply term_div_full; Auto.
Apply full_coef with (cpol (a,b) p); Trivial.
Unfold z_monom.
Apply no_divQ_zero; Auto.
Simpl.
Symmetry.
Apply divis_im_divt with n; Trivial.
EAuto.
Apply full_coef with (cpol (a,b) p); Trivial.
Apply elim_red_exp with fi (cpol (a,b) p).
Apply red1_exp_simpl with (div_term t
(hterm fi)) (divQ (coef (cpol (a,b) p) t) (hcoef fi)); Trivial.
Apply term_div_full; Auto.
Apply full_coef with (cpol (a,b) p); Trivial.
Transitivity (term_mult (hterm fi) (div_term t (hterm fi))); Auto.
Apply divis_im_divt with n; Auto.
Apply full_coef with (cpol (a,b) p); Trivial.
Save.
Definition simetrico [A:Set;R:A -> A -> Prop; a,b:A] : Prop :=
(R b a).
Definition noetheriano := [A:Set][R:A -> A -> Prop]
(well_founded A (simetrico A R)).
Lemma buen_ord_red: (fi:pol_full)(noetheriano ? (inc_red fi)).
Red; Intros.
Apply wf_incl with Tpol_full.
Red; Intros.
Red in H.
Apply red_menor2 with fi; Trivial.
Apply Tpol_full_wf.
Save.
Definition inc_Red1: (list pol_full)->pol_full->pol_full->Prop :=
[F:(list pol_full)][p,q:pol_full] (Red1 (inc_list F) (inc p) (inc q)).
Lemma Red1_menor2: (F:(list pol_full))(f,g:pol_full)(inc_Red1 F f g)->(Tpol_full g f).
Intros.
Inversion H.
Elim (can_fun f0); Trivial; Intros.
Elim p; Intros.
Clear p.
Apply red_menor2 with (exist pol [x:pol](full_pol x) x H3).
Unfold inc_red.
Simpl.
Apply red_ext3 with f0; Auto.
Inversion H2; Auto.
Save.
Lemma buen_ord_red1: (F:(list pol_full))(noetheriano ? (inc_Red1 F)).
Red; Intros.
Apply wf_incl with Tpol_full.
Red; Intros.
Red in H.
Apply Red1_menor2 with F; Auto.
Apply Tpol_full_wf.
Save.
Index
This page has been generated by coqdoc