proposition: Theorem order_add : ∀ a b, (order (a + b)%ps ≥ Qbar.min (order a) (order b))%Qbar.
proof: Proof. intros a b. unfold Qbar.ge. set (k₁ := ps_polydo b). set (k₂ := ps_polydo a). set (v₁ := (ps_ordnum a * Zpos k₁)%Z). set (v₂ := (ps_ordnum b * Zpos k₂)%Z). set (n₁ := Z.to_nat (v₂ - Z.min v₁ v₂)). set (n₂ := Z.to_nat (v₁ - Z.min v₁ v₂)). pose proof (ps_adjust_eq K a n₂ k₁) as Ha. pose proof (ps_adjust_eq K b n₁ k₂) as Hb. rewrite Hb in |- * at 1. rewrite Ha in |- * at 1. rewrite eq_ps_add_add₂. unfold ps_add₂. unfold adjust_ps_from. fold k₁ k₂. fold v₁ v₂. rewrite Z.min_comm. fold n₁ n₂. remember (adjust_ps n₂ k₁ a) as pa eqn:Hpa . remember (adjust_ps n₁ k₂ b) as pb eqn:Hpb . unfold order; simpl. remember (ps_terms pa) as sa eqn:Hsa . remember (ps_terms pb) as sb eqn:Hsb . remember (series_order sa 0) as na eqn:Hna . remember (series_order sb 0) as nb eqn:Hnb . remember (series_order (sa + sb)%ser 0) as nc eqn:Hnc . symmetry in Hna, Hnb, Hnc. destruct na as [na| ]. destruct nb as [nb| ]. destruct nc as [nc| ]; [ simpl | constructor ]. apply Qbar.le_qfin. rewrite Hpa, Hpb; simpl. subst k₁ k₂ n₁ n₂; simpl. unfold cm_factor; simpl. subst v₁ v₂; simpl. unfold cm_factor; simpl. rewrite Pos.mul_comm. rewrite Qmin_same_den. unfold Qle; simpl. apply Z.mul_le_mono_nonneg_r; [ apply Pos2Z.is_nonneg | idtac ]. remember (ps_ordnum a * Zpos (ps_polydo b))%Z as ab. remember (ps_ordnum b * Zpos (ps_polydo a))%Z as ba. rewrite Z2Nat.id. rewrite Z2Nat.id. rewrite Z.sub_sub_distr. rewrite Z.sub_diag, Z.add_0_l. rewrite Z.sub_sub_distr. rewrite Z.sub_diag, Z.add_0_l. rewrite Z.add_min_distr_l. apply Z.add_le_mono_l. rewrite <- Nat2Z.inj_min. apply Nat2Z.inj_le. apply series_order_iff in Hna; simpl in Hna. apply series_order_iff in Hnb; simpl in Hnb. apply series_order_iff in Hnc; simpl in Hnc. remember ps_terms_add as f; simpl in Hnc; subst f. destruct Hna as (Hina, Hna). destruct Hnb as (Hinb, Hnb). destruct Hnc as (Hinc, Hnc). apply Nat.nlt_ge. intros Hc. apply Nat.min_glb_lt_iff in Hc. destruct Hc as (Hca, Hcb). apply Hina in Hca. apply Hinb in Hcb. rewrite Hca, Hcb in Hnc. rewrite rng_add_0_l in Hnc. apply Hnc; reflexivity. rewrite <- Z.sub_max_distr_l. rewrite Z.sub_diag. rewrite Z.max_comm, <- Z2Nat_id_max. apply Nat2Z.is_nonneg. rewrite <- Z.sub_max_distr_l. rewrite Z.sub_diag. rewrite <- Z2Nat_id_max. apply Nat2Z.is_nonneg. destruct nc as [nc| ]; [ simpl | constructor ]. apply Qbar.le_qfin. unfold Qle; simpl. apply Z.mul_le_mono_pos_r; [ apply Pos2Z.is_pos | idtac ]. apply Z.add_le_mono_l. apply Nat2Z.inj_le. apply series_series_order_inf_iff in Hnb. rewrite Hnb in Hnc. rewrite rng_add_0_r in Hnc. rewrite Hna in Hnc. injection Hnc; intros; subst na; reflexivity. simpl. apply series_series_order_inf_iff in Hna. rewrite Hna in Hnc. rewrite rng_add_0_l in Hnc. rewrite Hnb in Hnc; subst nc. destruct nb as [nb| ]; [ idtac | constructor ]. apply Qbar.le_qfin. rewrite Hpa, Hpb; simpl. subst k₁ k₂ n₁ n₂; simpl. unfold cm_factor; simpl. subst v₁ v₂; simpl. unfold cm_factor; simpl. rewrite Pos.mul_comm. unfold Qle; simpl. apply Z.mul_le_mono_pos_r; [ apply Pos2Z.is_pos | idtac ]. apply Z.add_le_mono_r. rewrite Z2Nat.id. rewrite Z2Nat.id. do 2 rewrite Z.sub_sub_distr. do 2 rewrite Z.sub_diag; simpl. reflexivity. rewrite <- Z.sub_max_distr_l. rewrite Z.sub_diag. rewrite <- Z2Nat_id_max. apply Nat2Z.is_nonneg. rewrite <- Z.sub_max_distr_l. rewrite Z.sub_diag. rewrite Z.max_comm. rewrite <- Z2Nat_id_max. apply Nat2Z.is_nonneg. 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