proposition: Theorem ps_lap_in_add : ∀ 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_add in Hlab. destruct (ps_lap_nilp la) as [Hlaz| Hlanz]. rewrite Hlaz in Hlab. rewrite lap_add_nil_l in Hlab. apply Hlb; assumption. destruct (ps_lap_nilp lb) as [Hlbz| Hlbnz]. rewrite Hlbz in Hlab. rewrite lap_add_nil_r in Hlab. apply Hla; assumption. revert lb Hlb Hlab Hlbnz. induction la as [| a]; intros. simpl in Hlab. apply Hlb; assumption. rename m into n. simpl in Hlab. destruct lb as [| b]; [ apply Hla; assumption | idtac ]. simpl in Hlab. destruct Hlab as [(Hlab, Hab)| Hlab]. rewrite <- Hab. pose proof (order_add a b) as H. assert (order a > 0)%Qbar as Ha. apply Hla. left; split; [ assumption | reflexivity ]. assert (order b > 0)%Qbar as Hb. apply Hlb. left; split; [ assumption | reflexivity ]. unfold Qbar.ge in H. unfold Qbar.gt in Ha, Hb. destruct (Qbar.min_dec (order a) (order b)) as [Hoab| Hoab]. rewrite Hoab in H. eapply Qbar.lt_le_trans; [ idtac | eassumption ]. assumption. rewrite Hoab in H. eapply Qbar.lt_le_trans; [ idtac | eassumption ]. assumption. destruct (ps_zerop _ a) as [Haz| Hanz]. rewrite Haz in Hlanz. destruct (ps_zerop _ b) as [Hbz| Hbnz]. rewrite Hbz in Hlbnz. eapply IHla. intros m Hm; apply Hla; right; assumption. intros HH; apply Hlanz. constructor; [ reflexivity | assumption ]. intros m Hm; apply Hlb; right; eassumption. assumption. intros HH; apply Hlbnz. constructor; [ reflexivity | assumption ]. clear Hlbnz. destruct (ps_lap_nilp lb) as [Hlbz| Hlbnz]. rewrite Hlbz in Hlab. rewrite lap_add_nil_r in Hlab. apply Hla; right; assumption. eapply IHla. intros m Hm; apply Hla; right; assumption. intros HH; apply Hlanz. constructor; [ reflexivity | assumption ]. intros m Hm; apply Hlb; right; eassumption. assumption. assumption. destruct (ps_zerop _ b) as [Hbz| Hbnz]. rewrite Hbz in Hlbnz. clear Hlanz. destruct (ps_lap_nilp la) as [Hlaz| Hlanz]. rewrite Hlaz in Hlab. rewrite lap_add_nil_l in Hlab. apply Hlb; right; assumption. eapply IHla. intros m Hm; apply Hla; right; assumption. assumption. intros m Hm; apply Hlb; right; eassumption. assumption. intros HH; apply Hlbnz. constructor; [ reflexivity | assumption ]. clear Hlanz. clear Hlbnz. destruct (ps_lap_nilp la) as [Hlaz| Hlanz]. rewrite Hlaz in Hlab. rewrite lap_add_nil_l in Hlab. apply Hlb; right; assumption. destruct (ps_lap_nilp lb) as [Hlbz| Hlbnz]. rewrite Hlbz in Hlab. rewrite lap_add_nil_r in Hlab. apply Hla; right; assumption. eapply IHla. intros m Hm; apply Hla; right; assumption. assumption. intros m Hm; apply Hlb; right; eassumption. assumption. 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