Library impl_large
Require Export red_expl.
Lemma basic3_full: (h,f,g:pol)(F:(list pol_full))
(Red1 (inc_list F) f g)->(full_term_pol h)->
(x,y:pol_full)(equpol (inc x) (suma_app f h))->
(equpol (inc y) (suma_app g h))->(common_succ_full F x y).
Intros.
Elim basic3 with h f g (inc_list F); Trivial; Intros.
Elim (can_fun p); Trivial; Intros.
Elim p0; Intros.
Clear p0.
Split with (exist pol [x:pol](full_pol x) x0 H5); Simpl.
Apply Red3_ext1 with p; Auto.
Apply Red3_ext2 with (suma_app f h); Auto.
Simpl.
Apply Red3_ext2 with (suma_app g h); Auto.
Apply Red3_ext1 with p; Auto.
Inversion H3; Auto.
Save.
Lemma basic4_full: (f,g:pol_full)(F:(list pol_full))
(Red3 (inc_list F) (suma_app (inc f) (pol_opp (inc g))) vpol)->
(common_succ_full F f g).
Intros.
Elim basic4 with (inc f) (inc g) (inc_list F); Auto; Intros.
Elim (can_fun p); Trivial; Intros.
Elim p0; Intros.
Clear p0.
Split with (exist pol [x:pol](full_pol x) x H2); Simpl.
Apply Red3_ext1 with p; Auto.
Apply Red3_ext1 with p; Auto.
Inversion H0; Auto.
Save.
Lemma G2_impl_G3_LCR_full: (F:(list pol_full))(Groebner2_full F)->
((f,g,h:pol_full)(Red1 (inc_list F) (inc f) (inc g))->
(Red1 (inc_list F) (inc f) (inc h))->(common_succ_full F g h)).
Intros F Gb2.
Induction 1; Intros fF fi pfiF rfifg.
Induction 1; Intros fF' fj pfjF rfjfh.
Inversion rfifg.
Inversion rfjfh.
Clear H0 fF' H.
Cut (full n t).
Intro ft.
Cut (full n t0).
Intros ft0.
Cut (full_term_pol (cpol ((coef (inc f) t0),t0) vpol)).
Intros fct.
Cut (full_term_pol (cpol ((coef (inc f) t),t) vpol)).
Intros fct0.
Cut (full n (div_term t (hterm fi))).
Intros ftht.
Cut (full_term_pol
(mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))).
Intros fficht.
Cut (full_term_pol (suma_app (cpol ((coef (inc f) t),t) vpol) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))).
Intros fsucfi.
Cut (full n (div_term t0 (hterm fj))).
Intros ftht0.
Cut (full_term_pol
(mult_m fj ((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))).
Intros ffjcht.
Cut (full_term_pol (suma_app (cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))).
Intros fsucfj.
Cut (t=(hterm (cpol ((coef (inc f) t),t) vpol))).
Intros htt.
Cut (t0=(hterm (cpol ((coef (inc f) t0),t0) vpol))).
Intros htt0.
Elim (Ttm_total t0 t n); Trivial.
Destruct 1; Intros.
Clear a.
Elim split_pol with (inc f) t; Trivial.
Intros f1 hf1.
Elim hf1; Intros ff1 f1t'.
Clear hf1.
Intro.
Cut (full_term_pol (suma_app f1 (suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))))).
Intros ff1cfi.
Elim H; Intros f2 hf2 eqf.
Elim hf2; Intros ff2 htermf2.
Clear hf2.
Clear H.
Cut (full_term_pol (suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))).
Intros ff2cfj.
Cut (red fi (cpol ((coef (inc f) t),t) vpol)
(suma_app (cpol ((coef (inc f) t),t) vpol) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))); Intros.
Cut (red fj f2
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef f2 t0) (hcoef fj)),(div_term t0 (hterm fj))))))); Intros.
Cut (equpol (inc g) (suma_app (suma_app f1 (suma_app (cpol ((coef (inc f) t),t) vpol) f2))
(pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))); Intros.
Cut (equpol (inc g) (suma_app (suma_app f1 (suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))) f2)); Intros.
Cut (equpol (inc h) (suma_app (suma_app f1 (cpol ((coef (inc f) t),t) vpol))
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))); Intros.
Cut (red fi (inc h) (suma_app (suma_app f1 (suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))))
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))); Intros.
Elim (can_fun (suma_app (suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))) f2)); Trivial; Intros.
Elim p; Intros.
Clear p.
Elim (can_fun (suma_app (suma_app f1 (suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))))
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))); Trivial; Intros.
Elim p; Intros.
Clear p.
Cut (common_succ_full F (exist pol [x:pol](full_pol x) x H19)
(exist pol [x:pol](full_pol x) x0 H21)); Intros.
Apply comp_common_succ_full with p:=(exist pol [x:pol](full_pol x) x H19) r:=h; Auto.
Simpl.
Apply equpol_tran
with (suma_app
(suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi))))))) f2); Auto.
Apply trans_common_red_full
with f:=(exist pol [x:pol](full_pol x) x0 H21).
Apply Red1_simp with f:=fi; Auto.
Simpl.
Apply red_ext1
with (suma_app
(suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi)))))))
(suma_app f2
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj))))))); Auto.
Trivial.
Elim (can_fun (suma_app f2 (suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))))); Trivial; Intros.
Elim p; Intros.
Clear p.
Elim (can_fun (suma_app (suma_app f2
(pol_opp (mult_m fj ((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))
(suma_app f1 (suma_app (cpol ((coef (inc f) t),t) vpol) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))))); Trivial; Intros.
Elim p; Intros.
Clear p.
Apply comp_common_succ_full with p:=(exist pol [x:pol](full_pol x) x1 H23) r:=(exist pol [x:pol](full_pol x) x2 H25); Auto.
Simpl.
Apply equpol_tran
with (suma_app f2
(suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi)))))))); Auto.
Apply equpol_tran
with (suma_app
(suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi))))))) f2); Auto.
Simpl.
Apply equpol_tran
with (suma_app
(suma_app f2
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj))))))
(suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi)))))))); Auto.
Apply equpol_tran
with (suma_app
(suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi)))))))
(suma_app f2
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj))))))); Auto.
Apply basic3_full
with h:=(suma_app f1
(suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi))))))) f:=f2
g:=(suma_app f2
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj)))))).
Apply Red1_simp with fj; Trivial.
Apply red_ext1
with (suma_app f2
(pol_opp
(mult_m fj
((divQ (coef f2 t0) (hcoef fj)),(div_term t0 (hterm fj))))));
Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Trivial.
Apply eg_denomQ; Auto.
Apply coef_Ttm_split_pol with f1:=f1 t:=t; Trivial.
Apply full_term_suma_app; Trivial.
Simpl.
Auto.
Simpl.
Auto.
Apply full_term_suma_app; Trivial.
Apply full_term_suma_app; Trivial.
Apply full_term_suma_app; Trivial.
Apply full_term_suma_app; Trivial.
Apply red_ext2 with (suma_app (suma_app (cpol ((coef (inc f) t),t) vpol)
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))) f1); Trivial.
Apply equpol_sym.
Apply equpol_tran with (suma_app (suma_app f1 (cpol ((coef (inc f) t),t) vpol))
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))); Trivial.
Apply equpol_tran with (suma_app f1 (suma_app (cpol ((coef (inc f) t),t) vpol)
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))); Auto.
Apply red_ext1 with (suma_app (suma_app (suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))) f1).
Apply equpol_tran with (suma_app f1 (suma_app (suma_app (cpol ((coef (inc f) t),t) vpol)
(pol_opp (mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))); Auto.
Apply full_term_suma_app; Trivial.
Apply basic2; Trivial.
Apply hred_suma_bis; Trivial.
Apply hred1_simpl; Trivial.
Apply n_zmonom_n_vpol; Auto.
Replace (hterm (cpol ((coef (inc f) t),t) vpol)) with t; Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split.
Replace (hterm (cpol ((coef (inc f) t),t) vpol)) with t; Trivial.
Apply eg_denomQ; Auto.
Intros.
Replace (hterm (cpol ((coef (inc f) t),t) vpol)) with t.
Apply no_hterm_Ttm_in_red_bis with f2 (suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))) fj; Trivial.
Apply red_ext1 with (suma_app f2 (pol_opp (mult_m fj
((divQ (coef f2 t0) (hcoef fj)),(div_term t0 (hterm fj)))))); Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Trivial.
Apply eg_denomQ; Auto.
Apply coef_Ttm_split_pol with f1:=f1 t:=t; Trivial.
Intros.
Cut (Ttm t t2); Intros.
Cut (term_in_pol (cpol ((coef (inc f) t),t) vpol) t') \/
(term_in_pol (suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))) t'); Intros.
Elim H21; Intros.
Cut t=t'; Intros.
Rewrite <- H23; Auto.
Symmetry.
Apply eq_term_in_pol_monom with (coef (inc f) t); Trivial.
Apply full_coef with (cpol ((coef (inc f) t),t) vpol); Trivial.
Clear H21.
Apply Ttm_trans with t n; Trivial.
Cut (term_in_pol f2 t')\/(term_in_pol (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))) t'); Intros.
Elim H21; Intros; Clear H21; Auto.
Clear H22.
Cut (term_in_pol (mult_m fj ((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj)))) t'); Intros.
Apply term_in_Ttm with fj t0 (coef (inc f) t0); Trivial.
Apply full_coef with (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))); Trivial.
Apply term_in_pol_opp; Auto.
Apply term_in_sum; Trivial.
Apply full_coef with (suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))); Trivial.
Apply full_coef with f1; Trivial.
Apply term_in_sum; Trivial.
Auto.
Apply equpol_tran with (suma_app (inc f) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))); Trivial.
Apply equpol_tran with (suma_app (suma_app f1 (suma_app
(cpol ((coef (inc f) t),t) vpol) f2)) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))).
Apply equpol_ss; Trivial.
Apply equpol_tran with (suma_app (suma_app (suma_app f1
(cpol ((coef (inc f) t),t) vpol)) f2) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))); Auto.
Apply equpol_tran with (suma_app (inc f) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Trivial.
Apply equpol_tran with (suma_app (suma_app f1 (suma_app
(cpol ((coef (inc f) t),t) vpol) f2)) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))).
Apply equpol_ss; Trivial.
Apply equpol_tran with (suma_app (suma_app (suma_app f1
(cpol ((coef (inc f) t),t) vpol)) f2) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))).
Apply equpol_ss; Trivial.
Auto.
Apply equpol_tran with (suma_app (suma_app (suma_app f1
(cpol ((coef (inc f) t),t) vpol)) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))) f2).
Apply equpol_tran with (suma_app (suma_app f1 (cpol ((coef (inc f) t),t) vpol))
(suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))); Trivial.
Apply equpol_tran with (suma_app (suma_app f1 (cpol ((coef (inc f) t),t) vpol))
(suma_app (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))) f2)); Auto.
Apply equpol_ss; Trivial.
Apply equpol_tran with (suma_app (inc f) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Auto.
Apply red1_simpl with t0; Auto.
Apply split_term_in_pol with f1 (coef (inc f) t) t;Trivial.
Apply comp_term_in_pol with (inc f); Trivial.
Apply red1_simpl with t; Trivial.
Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Trivial.
Elim (eq_tm_dec t t); Intros; Auto.
Elim b; Auto.
Apply full_term_suma_app; Trivial.
Apply full_term_opp.
Apply full_mult_m; Trivial.
Apply full_term_suma_app; Trivial.
Apply conmt_common_succ_full.
Clear a.
Elim split_pol with (inc f) t0; Trivial; Intros f1 hf1.
Elim hf1; Intros ff1 f1t'.
Clear hf1.
Intro.
Elim H; Intros f2 hf2 eqf.
Elim hf2; Intros ff2 htermf2.
Clear hf2.
Clear H.
Cut (full_term_pol (suma_app f1 (suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp (mult_m fj((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))).
Intros ff1cfj.
Cut (full_term_pol (suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))).
Intros ff2cfi.
Cut (red fj (cpol ((coef (inc f) t0),t0) vpol) (suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))); Intros.
Cut (red fi f2 (suma_app f2 (pol_opp (mult_m fi
((divQ (coef f2 t) (hcoef fi)),(div_term t (hterm fi))))))); Intros.
Cut (equpol (inc g) (suma_app
(suma_app f1 (suma_app (cpol ((coef (inc f) t0),t0) vpol) f2))
(pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))); Intros.
Cut (equpol (inc h) (suma_app (suma_app f1 (cpol ((coef (inc f) t0),t0) vpol))
(suma_app f2 (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))); Intros.
Cut (equpol (inc h) (suma_app (suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))) f2)); Intros.
Cut (red fj (inc g) (suma_app (suma_app f1 (suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))))
(suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))))); Intros.
Elim (can_fun (suma_app f2 (suma_app f1 (suma_app
(cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))))); Trivial; Intros.
Elim p; Intros.
Clear p.
Elim (can_fun (suma_app (suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))
(suma_app f1 (suma_app (cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))))); Trivial; Intros.
Elim p; Intros.
Clear p.
Cut (common_succ_full F (exist pol [x:pol](full_pol x) x H19)
(exist pol [x:pol](full_pol x) x0 H21)); Intros.
Apply comp_common_succ_full with p:=(exist pol [x:pol](full_pol x) x H19) r:=g; Auto.
Simpl.
Apply equpol_sym.
Apply equpol_tran with (suma_app f2
(suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj)))))))); Auto.
Apply equpol_tran with (suma_app
(suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj))))))) f2); Auto.
Apply trans_common_red_full
with f:=(exist pol [x:pol](full_pol x) x0 H21).
Apply Red1_simp with f:=fj; Auto.
Simpl.
Apply red_ext1
with (suma_app
(suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj)))))))
(suma_app f2
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi))))))); Auto.
Apply equpol_tran with (suma_app
(suma_app f2
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi))))))
(suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj)))))))); Auto.
Auto.
Elim (can_fun (suma_app f2 (suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))))); Trivial; Intros.
Elim p; Intros.
Clear p.
Elim (can_fun (suma_app (suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))
(suma_app f1 (suma_app (cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))))); Trivial; Intros.
Elim p; Intros.
Clear p.
Apply comp_common_succ_full with p:=(exist pol [x:pol](full_pol x) x1 H23) r:=(exist pol [x:pol](full_pol x) x2 H25); Auto.
Simpl.
Apply equpol_tran with (suma_app f2
(suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj)))))))); Auto.
Simpl.
Apply equpol_tran with (suma_app
(suma_app f2
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi))))))
(suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj)))))))); Auto.
Apply basic3_full
with h:=(suma_app f1
(suma_app (cpol ((coef (inc f) t0),t0) vpol)
(pol_opp
(mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),
(div_term t0 (hterm fj))))))) f:=f2
g:=(suma_app f2
(pol_opp
(mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),
(div_term t (hterm fi)))))).
Apply Red1_simp with fi; Trivial.
Apply red_ext1 with (suma_app f2 (pol_opp (mult_m fi
((divQ (coef f2 t) (hcoef fi)),(div_term t (hterm fi)))))); Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Trivial.
Apply eg_denomQ; Auto.
Apply coef_Ttm_split_pol with f1:=f1 t:=t0; Trivial.
Apply full_term_suma_app; Trivial.
Simpl.
Auto.
Simpl; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_suma_app; Auto.
Apply red_ext2 with (suma_app (suma_app (cpol ((coef (inc f) t0),t0) vpol)
(suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))) f1); Trivial.
Apply equpol_sym.
Apply equpol_tran with (suma_app (suma_app f1 (suma_app
(cpol ((coef (inc f) t0),t0) vpol) f2)) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Trivial.
Apply equpol_tran with (suma_app f1 (suma_app
(cpol ((coef (inc f) t0),t0) vpol) (suma_app f2 (pol_opp
(mult_m fi ((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))))); Trivial.
Apply equpol_tran with (suma_app (suma_app f1 (suma_app
(cpol ((coef (inc f) t0),t0) vpol) f2)) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Trivial.
Apply equpol_tran with (suma_app (suma_app f1
(cpol ((coef (inc f) t0),t0) vpol)) (suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))); Trivial.
Apply equpol_tran with (suma_app (suma_app (suma_app f1
(cpol ((coef (inc f) t0),t0) vpol)) f2) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Auto.
Apply red_ext1 with (suma_app (suma_app (suma_app
(cpol ((coef (inc f) t0),t0) vpol)
(pol_opp (mult_m fj ((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))
(suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))) f1).
Apply equpol_tran with (suma_app f1 (suma_app (suma_app
(cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))
(suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))))); Auto.
Apply full_term_suma_app; Auto.
Apply basic2; Trivial.
Apply hred_suma_bis.
Apply hred1_simpl; Trivial.
Apply n_zmonom_n_vpol; Auto.
Replace (hterm (cpol ((coef (inc f) t0),t0) vpol)) with t0; Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split.
Replace (hterm (cpol ((coef (inc f) t0),t0) vpol)) with t0; Trivial.
Apply eg_denomQ; Auto.
Apply full_term_suma_app; Trivial.
Apply full_term_opp; Trivial.
Intros.
Replace (hterm (cpol ((coef (inc f) t0),t0) vpol)) with t0.
Apply no_hterm_Ttm_in_red_bis with f2 (suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))) fi; Trivial.
Apply red_ext1 with (suma_app f2 (pol_opp (mult_m fi
((divQ (coef f2 t) (hcoef fi)),(div_term t (hterm fi)))))); Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Trivial.
Apply eg_denomQ; Auto.
Apply coef_Ttm_split_pol with f1:=f1 t:=t0; Trivial.
Intros.
Cut (Ttm t0 t2); Intros.
Cut (term_in_pol (cpol ((coef (inc f) t0),t0) vpol) t')\/
(term_in_pol (suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))) t');Intros.
Elim H21; Intros.
Cut t0=t'; Intros.
Rewrite <- H23; Auto.
Symmetry.
Apply eq_term_in_pol_monom with (coef (inc f) t0);Trivial.
Apply full_coef with (cpol ((coef (inc f) t0),t0) vpol); Trivial.
Clear H21.
Apply Ttm_trans with t0 n; Trivial.
Cut (term_in_pol f2 t')\/(term_in_pol (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))) t'); Intros.
Elim H21; Intros; Clear H21; Auto.
Clear H22.
Cut (term_in_pol (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))) t'); Intros.
Apply term_in_Ttm with fi t (coef (inc f) t);Trivial.
Apply full_coef with (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))); Trivial.
Auto.
Apply term_in_sum; Trivial.
Apply full_coef with (suma_app f2 (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Trivial.
Apply full_coef with f1; Trivial.
Apply term_in_sum; Trivial.
Auto.
Apply equpol_tran with (suma_app (inc f) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))); Trivial.
Apply equpol_tran with (suma_app (suma_app f1 (suma_app
(cpol ((coef (inc f) t0),t0) vpol) f2))
(pol_opp (mult_m fj ((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))).
Apply equpol_ss; Auto.
Apply equpol_tran with (suma_app f1 (suma_app (suma_app
(cpol ((coef (inc f) t0),t0) vpol) f2) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))); Trivial.
Apply equpol_tran with (suma_app f1 (suma_app (suma_app
(cpol ((coef (inc f) t0),t0) vpol) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))) f2)).
Apply equpol_ss; Trivial.
Apply equpol_tran with (suma_app (cpol ((coef (inc f) t0),t0) vpol) (suma_app f2 (pol_opp
(mult_m fj ((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))))); Trivial.
Apply equpol_tran with (suma_app (cpol ((coef (inc f) t0),t0) vpol)
(suma_app (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj))))) f2)); Auto.
Auto.
Apply equpol_tran with (suma_app (inc f) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))); Trivial.
Apply equpol_tran with (suma_app (suma_app (suma_app f1
(cpol ((coef (inc f) t0),t0) vpol)) f2) (pol_opp (mult_m fj
((divQ (coef (inc f) t0) (hcoef fj)),(div_term t0 (hterm fj)))))); Trivial.
Apply equpol_ss; Trivial.
Apply equpol_tran with
(suma_app f1 (suma_app (cpol ((coef (inc f) t0),t0) vpol) f2)); Auto.
Apply equpol_tran with (suma_app (inc f) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Auto.
Apply red1_simpl with t; Trivial.
Apply split_term_in_pol with f1 (coef (inc f) t0) t0;Trivial.
Apply comp_term_in_pol with (inc f); Trivial.
Apply full_term_suma_app; Trivial.
Apply full_term_opp.
Apply full_mult_m; Trivial.
Apply red1_simpl with t0; Trivial.
Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Trivial.
Elim (eq_tm_dec t0 t0); Auto; Intros.
Elim b; Auto.
Apply full_term_suma_app; Trivial.
Apply full_term_opp; Trivial.
Apply full_term_suma_app; Trivial.
Intro.
Rewrite b in H14.
Rewrite b in H13.
Cut (equpol (suma_app (inc g) (pol_opp (inc h))) (mult_m (S_pol fj fi)
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi)))))); Intros.
Red in Gb2. Elim Gb2; Intros.
Clear H0.
Apply basic4_full; Trivial.
Apply Red3_ext2
with (mult_m (S_pol fj fi)
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi)))));
Auto.
Apply Red3_vpol_mult_m.
Elim (can_fun fj); Trivial; Intros.
Elim p; Intros.
Clear p.
Elim (can_fun fi); Trivial; Intros.
Elim p; Intros.
Clear p.
Cut (Red3 (inc_list F)
(S_pol (inc (exist pol [x:pol](full_pol x) x H0))
(inc (exist pol [x:pol](full_pol x) x0 H17))) vpol); Intros.
Simpl in H19.
Apply Red3_ext2 with (S_pol x x0); Auto.
Apply S_pol_ext; Auto.
Cut ~(equpol fj vpol); Intros.
EAuto.
Apply elem_n_vpol with (inc_list F); Auto.
Cut ~(equpol fi vpol); Intros.
EAuto.
Apply elem_n_vpol with (inc_list F); Auto.
Apply full_term_S_pol; Auto.
Apply H15.
Simpl.
Apply pol_In_ensemb_ext with fj; Auto.
Simpl.
Apply pol_In_ensemb_ext with fi; Auto.
Auto.
Apply equpol_tran with (suma_app (suma_app (inc f) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))
(pol_opp ((suma_app (inc f) (pol_opp (mult_m fj
((divQ (coef (inc f) t) (hcoef fj)),(div_term t (hterm fj))))))))).
Apply equpol_ss; Trivial.
Apply opp_comp; Trivial.
Apply equpol_tran with (suma_app (suma_app (inc f) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))
(suma_app (mult_m fj
((divQ (coef (inc f) t) (hcoef fj)),(div_term t (hterm fj)))) (pol_opp (inc f)))).
Auto.
Apply equpol_tran with (suma_app (suma_app (mult_m fj
((divQ (coef (inc f) t) (hcoef fj)),(div_term t (hterm fj))))
(pol_opp (inc f))) (suma_app (inc f) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi))))))); Trivial.
Apply equpol_tran with (suma_app (mult_m fj
((divQ (coef (inc f) t) (hcoef fj)),(div_term t (hterm fj)))) (pol_opp (mult_m fi
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))))); Trivial.
Unfold S_pol.
Apply equpol_tran with (suma_app (mult_m (mult_m fj
((divQ unQ (hcoef fj)),(div_term (lcm (hterm fj) (hterm fi)) (hterm fj))))
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi))))) (mult_m (pol_opp (mult_m fi
((divQ unQ (hcoef fi)),(div_term (lcm (hterm fj) (hterm fi)) (hterm fi)))))
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi)))))).
Apply equpol_ss.
Apply equpol_tran with (mult_m fj (mult_mon
((divQ unQ (hcoef fj)),(div_term (lcm (hterm fj) (hterm fi)) (hterm fj)))
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi)))))).
Apply mult_pm_comp_2.
Simpl.
Right.
Split.
Apply simpl_term with n; Auto.
Apply lcm_div with n; Auto.
Apply eqQ_trans with (divQ (multQ unQ (coef (inc f) t)) (hcoef fj)); Auto.
Apply eg_denomQ; Auto.
Apply eqQ_sym.
Apply eqQ_trans with (multQ (coef (inc f) t) unQ); Auto.
Auto.
Apply equpol_tran with (mult_m (pol_opp fi)
((divQ (coef (inc f) t) (hcoef fi)),(div_term t (hterm fi)))); Trivial.
Apply equpol_tran with (pol_opp (mult_m (mult_m fi
((divQ unQ (hcoef fi)),(div_term (lcm (hterm fj) (hterm fi)) (hterm fi))))
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi)))))); Trivial.
Apply equpol_tran with (pol_opp (mult_m fi (mult_mon
((divQ unQ (hcoef fi)),(div_term (lcm (hterm fj) (hterm fi)) (hterm fi)))
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi))))))).
Apply equpol_tran with (mult_m (pol_opp fi) (mult_mon
((divQ unQ (hcoef fi)),(div_term (lcm (hterm fj) (hterm fi)) (hterm fi)))
((coef (inc f) t),(div_term t (lcm (hterm fj) (hterm fi)))))).
Apply mult_pm_comp_2.
Simpl.
Right.
Split.
Apply simpl_term with n; Auto.
Apply lcm_div with n; Auto.
Apply eqQ_trans with (divQ (multQ unQ (coef (inc f) t)) (hcoef fi)); Auto.
Apply eg_denomQ; Auto.
Apply eqQ_sym.
Apply eqQ_trans with (multQ (coef (inc f) t) unQ); Auto.
Auto.
Auto.
Cut ~(equpol fi vpol); Intros.
Cut ~(equpol fj vpol); Intros.
Generalize fi fj H H0.
Induction fi0; Intros.
Elim H15; Auto.
Induction fj0; Intros.
Elim H17; Auto.
Simpl; Auto.
Apply elem_n_vpol with (inc_list F); Trivial.
Apply elem_n_vpol with (inc_list F); Trivial.
Symmetry.
Apply term_monom_hterm; Auto.
Symmetry.
Apply term_monom_hterm; Auto.
Apply full_term_suma_app; Trivial.
Apply full_term_opp; Trivial.
Apply full_mult_m; Trivial.
Apply term_div_full; Auto.
Apply full_term_suma_app; Trivial.
Apply full_term_opp; Trivial.
Apply full_mult_m; Trivial.
Apply term_div_full; Auto.
Apply full_term_pol_cons; Trivial.
Apply full_term_pol_cons; Trivial.
Apply full_coef with (inc f); Trivial.
Apply full_coef with (inc f); Trivial.
Save.
Hints Resolve G2_impl_G3_LCR_full.
Index
This page has been generated by coqdoc