Library Div_poly_tes
Require Export ecuaciones_tes.
Fixpoint div_m [p:pol] : monom -> pol :=
[m:monom]Cases p of
vpol => vpol
| (cpol m1 p1) => (cpol (div_mon m1 m) (div_m p1 m))
end.
Lemma distr_div_suma: (m:monom)(p1,p2:pol)
(div_m (suma_app p1 p2) m)=(suma_app (div_m p1 m) (div_m p2 m)).
Induction p1; Simpl; Auto.
Intros.
Rewrite H; Auto.
Save.
Hints Resolve distr_div_suma.
Lemma div_mult_inv:
(m:monom)~(z_monom m)->(full_mon n m)
->(p:pol)(full_term_pol p)->(equpol (div_m (mult_m p m) m) p).
Induction 3; Simpl; Auto.
Generalize H H0.
Clear H H0.
Case m; Simpl; Intros.
Apply equpol_cpol2; Trivial.
Simpl.
Right.
Split.
Apply div_mult_mon_inv with n; Auto.
Apply eqQ_trans with (multQ unQ a).
Apply eqQ_trans with (multQ (divQ q q) a); Auto.
Apply eqQ_trans with (multQ a unQ); Auto.
Save.
Hints Resolve div_mult_inv.
Lemma div_pm_comp:(m:monom)~(z_monom m)->(f:pol)(equpol (mult_m f m) vpol)->(equpol (div_m (mult_m f m) m) (div_m vpol m)).
Induction 2; Intros; Trivial.
Auto.
Apply equpol_tran with (div_m q m); Auto.
Simpl.
Rewrite distr_div_suma.
Rewrite distr_div_suma.
Simpl; Auto.
Rewrite distr_div_suma.
Rewrite distr_div_suma; Auto.
Generalize H.
Case m; Intros.
Unfold z_monom in H1.
Simpl.
Apply equpol_tran
with (cpol ((plusQ (divQ k q) (divQ k' q)),(div_term t t0))
(div_m p (q,t0))); Auto.
Simpl.
Apply equpol_elim.
Generalize H H1.
Case m0; Case m; Simpl; Intros.
Apply divQ_0; Auto.
Save.
Hints Resolve div_pm_comp.
Lemma mult_nz_monom: (f:pol)(full_term_pol f)->
(m:monom)(full_mon n m)->~(z_monom m)->
(equpol (mult_m f m) vpol)->(equpol f vpol).
Intros.
Apply equpol_tran with (div_m (mult_m f m) m); Auto.
Replace vpol with (div_m vpol m); Auto.
Save.
Hints Resolve mult_nz_monom.
Lemma contr_mult_nz_monom: (f:pol)(full_term_pol f)->
(~(equpol f vpol))->(c:Q)(~(eqQ c OQ))->
(t:term)(full n t)->(~(equpol (mult_m f (c,t)) vpol)).
Red.
Intros.
Cut (equpol f vpol); Auto.
Apply mult_nz_monom with m:=(c,t); Auto.
Save.
Hints Resolve contr_mult_nz_monom.
Index
This page has been generated by coqdoc