Library Hmtc_axiom
Require Export S_poly_nuevo2_tes.
Lemma aux_no_hterm_Ttm_in_red: (f,g,fj:pol)(red fj f g)->
(Ttm (hterm g) (hterm f)) \/ (hterm g)=(hterm f).
Intros.
Elim (vpol_dec_full_term g).
Inversion H.
Intros.
Elim (vpol_dec_full_term f); Intros; Trivial.
Right.
Transitivity (hterm vpol).
Apply eq_hterm; Trivial.
Apply eq_hterm; Auto.
Elim (eq_tm_dec (hterm f) (n_term_O n)); Intros.
Right.
Rewrite a0.
Transitivity (hterm vpol).
Apply eq_hterm; Trivial.
Apply hterm_vpol.
Left.
Replace (hterm g) with (n_term_O n).
Apply ord_adm1; Auto.
Transitivity (hterm vpol).
Symmetry.
Apply hterm_vpol.
Apply eq_hterm; Auto.
Intro H0.
Inversion H; Intros.
Cut ~(equpol f vpol); Intros.
Cut ~(eqQ (coef f t) OQ); Intros.
Cut (full n t); Intros.
Cut (full_term_pol (pol_opp (mult_m fj
((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj)))))); Intros.
Cut t=(hterm f)\/(Ttm t (hterm f)); Intros.
Elim H12; Intros; Clear H12.
Left.
Rewrite H13 in H7.
Rewrite H13 in H6.
Replace (hterm g) with (hterm (suma_app f
(pol_opp (mult_m fj ((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj))))))).
Apply hterm_eq_suma_Ttm; Trivial.
Apply eq_nvpol with g; Trivial.
Rewrite H13; Auto.
Rewrite H13.
Apply eqQ_trans with (multQ_neg (hcoef (pol_opp f))).
Apply hcoef_pol_opp_term; Trivial.
Apply eq_mulQ_neg.
Apply eq_pol_opp_hcoef; Trivial.
Apply full_mult_m; Auto.
Apply eqQ_trans with (multQ (hcoef fj) (mon_coef
((divQ (coef f (hterm f)) (hcoef fj)),(div_term (hterm f) (hterm fj))))).
Apply hcoef_mult; Trivial.
Auto.
Simpl.
Apply eqQ_trans with (multQ (hcoef fj) (divQ (hcoef f) (hcoef fj))).
Apply multQ_comp_l; Auto.
Apply eqQ_trans with (multQ (divQ (hcoef f) (hcoef fj)) (hcoef fj)); Trivial.
Apply eqQ_trans with (divQ (multQ (hcoef f) (hcoef fj)) (hcoef fj)); Auto.
Apply eqQ_trans with (divQ (multQ (hcoef fj) (hcoef f)) (hcoef fj)); Auto.
Transitivity (hterm (pol_opp f)).
Apply hterm_pol_opp_term; Trivial.
Apply eq_pol_opp_hterm; Trivial.
Apply full_mult_m; Auto.
Transitivity (term_mult (hterm fj) (mon_term
((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj))))); Auto.
Simpl.
Rewrite H13.
Apply divis_im_divt with n; Auto.
Symmetry.
Apply hterm_mult_m; Trivial.
Simpl.
Apply term_div_full; Auto.
Simpl.
Apply no_divQ_zero; Auto.
Apply eq_hterm; Trivial.
Apply full_term_suma_app; Trivial.
Rewrite H13; Auto.
Right.
Replace (hterm g) with (hterm (suma_app f (pol_opp (mult_m fj
((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj))))))); Auto.
Apply hterm_suma_Ttm; Trivial.
Replace (hterm (pol_opp (mult_m fj
((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj)))))) with
(hterm (mult_m fj ((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj))))).
Replace (hterm (mult_m fj ((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj)))))
with (term_mult (hterm fj)
(mon_term ((divQ (coef f t) (hcoef fj)),(div_term t (hterm fj))))).
Simpl.
Replace (term_mult (hterm fj) (div_term t (hterm fj))) with t; Trivial.
Apply divis_im_divt with n; Auto.
Symmetry.
Apply hterm_mult_m; Trivial.
Simpl; Auto.
Simpl.
Apply no_divQ_zero; Auto.
Apply hterm_pol_opp_term.
Apply full_mult_m; Auto.
Elim (eq_tm_dec t (hterm f)); Intros.
Left; Trivial.
Right.
Apply Ttm_pol_hterm; Auto.
Apply full_term_opp.
Apply full_mult_m; Auto.
Apply full_coef with f; Trivial.
Auto.
Apply term_in_pol_nvpol with t; Auto.
Inversion H; Auto.
Save.
Lemma no_hterm_Ttm_in_red: (f,g,fj:pol)(t:term)(full n t)->(Ttm (hterm f) t)->
(red fj f g)->(Ttm (hterm g) t).
Intros.
Inversion H1.
Cut (Ttm (hterm g) (hterm f))\/(hterm g)=(hterm f); Intros.
Elim H9; Intros; Clear H9.
Apply Ttm_trans with (hterm f) n; Auto.
Rewrite <- H10 in H0; Auto.
Apply aux_no_hterm_Ttm_in_red with fj; Trivial.
Save.
Hints Resolve no_hterm_Ttm_in_red.
Lemma no_hterm_Ttm_in_red_bis: (f,g,fj:pol)(t:term)(full n t)->
((t1:term)(term_in_pol f t1)->(Ttm t1 t))->(red fj f g)->
((t2:term)(term_in_pol g t2)->(Ttm t2 t)).
Intros.
Inversion H1.
(Elim eq_tm_dec with t2 (hterm g); Intros).
Rewrite a.
Cut (Ttm (hterm f) t); Intros.
Cut ~(equpol g vpol); Intros.
(Apply no_hterm_Ttm_in_red with f fj; Auto).
EAuto.
EAuto.
Cut (Ttm (hterm f) t); Intros.
Cut ~(equpol g vpol); Intros.
(Apply Ttm_trans with (hterm g) n; Auto).
EAuto.
Apply no_hterm_Ttm_in_red with f fj; Auto.
EAuto.
EAuto.
Save.
Hints Resolve no_hterm_Ttm_in_red_bis.
Index
This page has been generated by coqdoc