Library ecuaciones_tes
Require Export Mult_poly_tes.
Lemma ch_m_plus: (p,q,r:pol)(m:monom)(equpol p
(suma_app q (pol_opp (mult_m r m))))->(equpol q (suma_app p (mult_m r m))).
Intros.
Apply equpol_sym.
Apply equpol_tran with (suma_app (suma_app q (pol_opp (mult_m r m))) (mult_m r m));
Auto.
Apply equpol_tran with (suma_app q vpol); Auto.
Apply equpol_tran with (suma_app q (suma_app (pol_opp (mult_m r m)) (mult_m r m)));
Auto.
Save.
Hints Resolve ch_m_plus .
Lemma ch_m_plus2: (p,q,r:pol)(m:monom)(equpol p
(suma_app q (pol_opp (mult_m r m))))->
(equpol (suma_app q (pol_opp p)) (mult_m r m)).
Intros.
Apply equpol_sym.
Apply equpol_tran with (suma_app (suma_app (mult_m r m) p) (pol_opp p)).
Apply equpol_sym.
Apply equpol_tran with (suma_app (mult_m r m) (suma_app p (pol_opp p))).
Auto.
(Apply equpol_tran with (suma_app (mult_m r m) vpol); Auto).
Apply equpol_ss.
Apply equpol_sym.
Apply equpol_tran
with (suma_app (suma_app q (mult_m r m)) (pol_opp (mult_m r m))).
Apply equpol_sym.
Apply equpol_tran
with (suma_app q (suma_app (mult_m r m) (pol_opp (mult_m r m)))).
Auto.
Apply equpol_tran with (suma_app q vpol).
Auto.
Auto.
Apply equpol_tran
with (suma_app (mult_m r m) (suma_app q (pol_opp (mult_m r m)))).
(Apply equpol_tran
with (suma_app (suma_app (mult_m r m) q) (pol_opp (mult_m r m)));
Auto).
Auto.
Auto.
Save.
Hints Resolve ch_m_plus2.
Lemma equat1: (p,q,r:pol)(equpol
(suma_app (suma_app p (pol_opp q)) (suma_app q (pol_opp r)))
(suma_app p (pol_opp r))).
Intros.
Apply equpol_tran
with (suma_app p (suma_app (pol_opp q) (suma_app q (pol_opp r)))).
Auto.
Apply equpol_tran
with (suma_app p (suma_app (suma_app (pol_opp q) q) (pol_opp r))).
Auto.
Apply equpol_tran with (suma_app p (suma_app vpol (pol_opp r))).
(Apply equpol_tran with (suma_app p (suma_app vpol (pol_opp r))); Auto).
(Apply equpol_ss; Auto).
Save.
Hints Resolve equat1.
Lemma mult_sum_opp2: (p,p',q,q':pol)(equpol p
(suma_app (mult_p q q') p'))->(equpol (pol_opp p)
(suma_app (mult_p q (pol_opp q')) (pol_opp p'))).
Intros.
Apply equpol_sym.
Apply (sum_vpol_opp (suma_app (mult_p q (pol_opp q')) (pol_opp p')) p).
Apply equpol_tran
with (suma_app (mult_p q (pol_opp q')) (suma_app (pol_opp p') p)).
Auto.
Apply equpol_tran
with (suma_app (mult_p q (pol_opp q'))
(suma_app (pol_opp p') (suma_app (mult_p q q') p'))).
Auto.
Apply equpol_tran
with (suma_app (mult_p q (pol_opp q'))
(suma_app (pol_opp p') (suma_app p' (mult_p q q')))).
Auto.
Apply equpol_tran
with (suma_app (mult_p q (pol_opp q'))
(suma_app (suma_app (pol_opp p') p') (mult_p q q'))).
Auto.
Apply equpol_tran
with (suma_app (mult_p q (pol_opp q')) (suma_app vpol (mult_p q q'))).
(Apply equpol_ss; Auto).
Apply equpol_tran with (suma_app (mult_p q (pol_opp q')) (mult_p q q')).
Auto.
Apply equpol_tran with (mult_p q (suma_app (pol_opp q') q')).
Auto.
Apply equpol_tran with (mult_p q vpol).
(Apply equpol_tran with (mult_p q (suma_app q' (pol_opp q'))); Auto).
Auto.
Save.
Hints Resolve mult_sum_opp2.
Lemma mult_sum_opp1: (f,g:pol)(equpol (suma_app g (pol_opp f))
(pol_opp (suma_app f (pol_opp g)))).
Intros.
Apply (sum_vpol_opp (suma_app g (pol_opp f)) (suma_app f (pol_opp g))).
Apply equpol_tran
with (suma_app (suma_app g (suma_app (pol_opp f) f)) (pol_opp g)).
(Apply equpol_tran
with (suma_app (suma_app (suma_app g (pol_opp f)) f) (pol_opp g));
Auto).
Apply equpol_tran with (suma_app (suma_app g vpol) (pol_opp g)).
Auto.
Apply equpol_tran with (suma_app g (pol_opp g)).
Auto.
Auto.
Save.
Hints Resolve mult_sum_opp1.
Lemma opp_mult_m: (p:pol)(m:monom)(equpol (pol_opp(mult_m p m))
(mult_m (pol_opp p) m)).
Intros.
Apply equpol_sym.
Apply sum_vpol_opp.
Apply equpol_tran with (mult_m (suma_app (pol_opp p) p) m).
Auto.
Apply equpol_tran with (mult_m (suma_app p (pol_opp p)) m).
Auto.
Apply equpol_tran with (mult_m vpol m).
Auto.
Auto.
Save.
Hints Resolve opp_mult_m.
Lemma ayuda_Benj: (y,y':Q)(y0:term)(p',q',r:pol)
(eqQ y (multQ_neg y'))->(equpol r (suma_app p' q'))->
(equpol r (suma_app (cpol (y,y0) p') (cpol (y',y0) q'))).
Intros.
Apply (equpol_tran r (suma_app p' q')
(suma_app (cpol (y,y0) p') (cpol (y',y0) q'))).
Auto.
Apply equpol_tran with (cpol ((plusQ y y'),y0) (suma_app p' q')).
Apply equpol_sym.
Apply equpol_elim.
Unfold z_monom.
Auto.
Apply equpol_sym.
Simpl.
(Apply equpol_tran with (cpol (y,y0) (cpol (y',y0) (suma_app p' q')));
Auto).
Save.
Hints Resolve ayuda_Benj.
Lemma ayud_Gilb: (y,y':Q)(y0:term)(p',q',r:pol)(equpol r (suma_app p' q'))
->(equpol (suma_app (cpol (y,y0) p') (cpol (y',y0) q'))
(cpol (y,y0) (cpol (y',y0) r))).
Intros.
Apply (equpol_tran (suma_app (cpol (y,y0) p') (cpol (y',y0) q'))
(cpol (y,y0) (cpol (y',y0) (suma_app p' q')))
(cpol (y,y0) (cpol (y',y0) r))).
Auto.
Auto.
Save.
Hints Resolve ayud_Gilb.
Index
This page has been generated by coqdoc