proposition: Theorem ps_lap_in_mul_ge : ∀ la lb, (∀ m, ps_lap_in m la → (order m ≥ 0)%Qbar) → (∀ m, ps_lap_in m lb → (order m ≥ 0)%Qbar) → (∀ m, ps_lap_in m (la * lb) → (order m ≥ 0)%Qbar).
proof: Proof. intros la lb Hla Hlb m Hlab. unfold ps_lap_mul in Hlab. revert m lb Hlb Hlab. induction la as [| a]; intros. rewrite lap_mul_nil_l in Hlab; contradiction. rewrite lap_mul_cons_l in Hlab. eapply ps_lap_in_add_ge; [ idtac | idtac | eassumption ]. intros n Hn. destruct (ps_zerop _ a) as [Ha| Ha]. rewrite Ha in Hn. rewrite lap_eq_0 in Hn. rewrite lap_mul_nil_l in Hn; contradiction. assert (order a ≥ 0)%Qbar as Hoa. apply Hla; left; split; [ idtac | reflexivity ]. intros H. apply lap_eq_cons_nil_inv in H. destruct H; contradiction. revert Hlb Hn Hoa; clear -K; intros. rewrite lap_mul_const_l in Hn. induction lb as [| b]; [ contradiction | idtac ]. simpl in Hn. destruct Hn as [(Hab, Hn)| Hn]. rewrite <- Hn, order_mul. eapply Qbar.le_trans; [ eassumption | idtac ]. apply Qbar.le_sub_le_add_l. rewrite Qbar.sub_diag. destruct (ps_zerop _ b) as [Hb| Hb]. rewrite Hb, order_0; constructor. apply Hlb; left; split; [ idtac | reflexivity ]. intros H; apply Hb. apply lap_eq_cons_nil_inv in H. destruct H; assumption. apply IHlb; [ idtac | assumption ]. intros p Hp. apply Hlb; right; assumption. intros n Hn. simpl in Hn. destruct Hn as [(Hab, Hn)| Hn]. symmetry in Hn. rewrite Hn, order_0; constructor. eapply IHla; try eassumption. intros p Hp. apply Hla; right; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Misc NbarM QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHull ConvexHullMisc PolyConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq