proposition: Theorem order_add_eq_min : ∀ a b, (order a ≠ order b)%Qbar → (order (a + b) = Qbar.min (order a) (order b))%Qbar.
proof: Proof. intros a b Hab. 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. symmetry. rewrite Hb in Hab. rewrite Ha in Hab. 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 . remember (order pa) as opa eqn:Hopa . remember (order pb) as opb eqn:Hopb . progress unfold order in Hopa, Hopb. progress 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. clear Hsa Hsb Ha Hb. 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. destruct na as [na| ]. destruct Hna as (Hina, Hna). destruct nb as [nb| ]. destruct Hnb as (Hinb, Hnb). subst pa pb; simpl in Hopa, Hopb; simpl. subst k₁ k₂ n₁ n₂; simpl in Hopa, Hopb; simpl. subst v₁ v₂; simpl in Hopa, Hopb. rewrite Pos.mul_comm in Hopb. rewrite Z2Nat.id in Hopa. rewrite Z2Nat.id in Hopb. rewrite Z.sub_sub_distr in Hopa, Hopb. rewrite Z.sub_diag, Z.add_0_l in Hopa, Hopb. unfold cm_factor; simpl. rewrite Z2Nat.id. rewrite Z.sub_sub_distr. rewrite Z.sub_diag, Z.add_0_l. subst opa opb; simpl. rewrite Qmin_same_den. unfold Qeq; simpl. simpl in Hab. unfold Qeq in Hab; simpl in Hab. destruct nc as [nc| ]. destruct Hnc as (Hinc, Hnc). apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | idtac ]. rewrite Z.add_min_distr_l. apply Z.add_cancel_l. rewrite <- Nat2Z.inj_min. apply Nat2Z.inj_iff. destruct (eq_nat_dec (min na nb) nc) as [| H]; [ assumption | idtac ]. exfalso; apply Hab; clear Hab. apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | idtac ]. apply Z.add_cancel_l. apply Nat2Z.inj_iff. destruct (eq_nat_dec na nb) as [| Hab]; [ assumption | idtac ]. exfalso; apply H; clear H. destruct (le_dec na nb) as [H₁| H₁]. apply Nat_le_neq_lt in H₁; [ idtac | assumption ]. destruct (lt_dec na nc) as [H₂| H₂]. apply Hinb in H₁. apply Hinc in H₂. rewrite H₁, rng_add_0_r in H₂; contradiction. apply Nat.nlt_ge in H₂. destruct (eq_nat_dec na nc) as [H₃| H₃]. rewrite Nat.min_l; [ assumption | idtac ]. apply Nat.lt_le_incl; assumption. apply Nat.neq_sym in H₃. apply Nat_le_neq_lt in H₂; [ idtac | assumption ]. eapply Nat.lt_trans in H₁; [ idtac | eassumption ]. apply Hina in H₂. apply Hinb in H₁. rewrite H₂, H₁ in Hnc. rewrite rng_add_0_l in Hnc. exfalso; apply Hnc; reflexivity. apply Nat.nle_gt in H₁. destruct (lt_dec nb nc) as [H₂| H₂]. apply Hina in H₁. apply Hinc in H₂. rewrite H₁, rng_add_0_l in H₂; contradiction. apply Nat.nlt_ge in H₂. destruct (eq_nat_dec nb nc) as [H₃| H₃]. rewrite Nat.min_r; [ assumption | idtac ]. apply Nat.lt_le_incl; assumption. apply Nat.neq_sym in H₃. apply Nat_le_neq_lt in H₂; [ idtac | assumption ]. eapply Nat.lt_trans in H₁; [ idtac | eassumption ]. apply Hinb in H₂. apply Hina in H₁. rewrite H₂, H₁ in Hnc. rewrite rng_add_0_l in Hnc. exfalso; apply Hnc; reflexivity. simpl in Hab. apply Hab; clear Hab. apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | idtac ]. apply Z.add_cancel_l. apply Nat2Z.inj_iff. destruct (eq_nat_dec na nb) as [| Hab]; [ assumption | idtac ]. destruct (le_dec na nb) as [H₁| H₁]. apply Nat_le_neq_lt in H₁; [ idtac | assumption ]. apply Hinb in H₁. pose proof (Hnc na) as H. rewrite H₁, rng_add_0_r in H. contradiction. apply Nat.nle_gt in H₁. apply Hina in H₁. pose proof (Hnc nb) as H. rewrite H₁, rng_add_0_l in H. contradiction. 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, <- 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. subst opb; simpl. rewrite Qbar.min_comm; simpl. destruct nc as [nc| ]. destruct Hnc as (Hinc, Hnc). subst opa. apply Qbar.qfin_inj_wd. unfold Qeq; simpl. apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | idtac ]. apply Z.add_cancel_l. apply Nat2Z.inj_iff. destruct (eq_nat_dec na nc) as [| Hac]; [ assumption | idtac ]. destruct (le_dec na nc) as [H₁| H₁]. apply Nat_le_neq_lt in H₁; [ idtac | assumption ]. apply Hinc in H₁. rewrite Hnb, rng_add_0_r in H₁. contradiction. apply Nat.nle_gt in H₁. apply Hina in H₁. rewrite H₁, Hnb, rng_add_0_l in Hnc. exfalso; apply Hnc; reflexivity. pose proof (Hnc na) as H. rewrite Hnb, rng_add_0_r in H. contradiction. subst opa; simpl. destruct nb as [nb| ]. destruct Hnb as (Hinb, Hnb). destruct nc as [nc| ]. destruct Hnc as (Hinc, Hnc). destruct (eq_nat_dec nb nc) as [| Hbc]; [ subst nb | idtac ]. subst. subst n₁ n₂ v₁ v₂ k₁ k₂; simpl. unfold cm_factor; simpl. rewrite Z2Nat.id. rewrite Z2Nat.id. do 2 rewrite Z.sub_sub_distr. do 2 rewrite Z.sub_diag, Z.add_0_l. rewrite Pos.mul_comm; 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, <- Z2Nat_id_max. apply Nat2Z.is_nonneg. destruct (le_dec nb nc) as [H₁| H₁]. apply Nat_le_neq_lt in H₁; [ idtac | assumption ]. apply Hinc in H₁. rewrite Hna, rng_add_0_l in H₁. contradiction. apply Nat.nle_gt in H₁. apply Hinb in H₁. rewrite Hna, rng_add_0_l in Hnc. contradiction. pose proof (Hnc nb) as H. rewrite Hna, rng_add_0_l in H. contradiction. subst opb. exfalso; apply Hab; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m