proposition: Theorem order_mul : ∀ a b, (order (a * b)%ps = order a + order b)%Qbar.
proof: Proof. intros a b. symmetry. pose proof (ps_adjust_eq K a 0 (ps_polydo b)) as Ha. pose proof (ps_adjust_eq K b 0 (ps_polydo a)) as Hb. rewrite Hb in |- * at 1. rewrite Ha in |- * at 1. unfold order; simpl. unfold cm_factor, cm; simpl. do 2 rewrite series_shift_0. remember (series_stretch (ps_polydo b) (ps_terms a)) as sa eqn:Hsa . remember (series_stretch (ps_polydo a) (ps_terms b)) 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. rewrite Z.sub_0_r. rewrite Z.sub_0_r. unfold Qeq; simpl. symmetry. rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. rewrite Z.mul_shuffle0. apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | idtac ]. symmetry. rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. rewrite Z.add_comm. rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. rewrite Z.mul_shuffle0. rewrite <- Z.mul_add_distr_r. rewrite <- Z.mul_add_distr_r. rewrite <- Z.mul_assoc. apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | idtac ]. rewrite Z.add_comm. rewrite Z.add_shuffle1. rewrite <- Z.add_assoc. rewrite <- Z.add_assoc. apply Z.add_cancel_l. apply Z.add_cancel_l. 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 Hna as (Hia, Hna). destruct Hnb as (Hib, Hnb). destruct Hnc as (Hic, Hnc). rewrite <- Nat2Z.inj_add. apply Nat2Z.inj_iff. destruct (lt_dec (na + nb) nc) as [Hlt| Hge]. apply Hic in Hlt. unfold convol_mul in Hlt. rewrite summation_only_one_non_0 with (v := na) in Hlt. rewrite Nat.add_comm, Nat.add_sub in Hlt. apply fld_eq_mul_0_l in Hlt; try assumption; contradiction. split; [ apply Nat.le_0_l | apply le_plus_l ]. intros i (_, Hiab) Hina. destruct (lt_dec i na) as [Hilt| Hige]. rewrite Hia; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. apply Nat.nlt_ge in Hige. rewrite Hib; [ rewrite rng_mul_0_r; reflexivity | idtac ]. apply Nat.add_lt_mono_r with (p := i). rewrite Nat.sub_add; auto with Arith. rewrite Nat.add_comm. apply Nat.add_lt_mono_l, Nat_le_neq_lt; auto with Arith. apply Nat.nlt_ge in Hge. destruct (lt_dec nc (na + nb)) as [Hclt| Hcge]. unfold convol_mul in Hnc. rewrite all_0_summation_0 in Hnc. exfalso; apply Hnc; reflexivity. intros h (_, Hhc). destruct (lt_dec h na) as [Hha| Hha]. rewrite Hia; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. destruct (lt_dec (nc - h) nb) as [Hhb| Hhb]. rewrite Hib; [ idtac | assumption ]. rewrite rng_mul_0_r; reflexivity. exfalso; apply Hhb; clear Hhb. apply Nat.add_lt_mono_r with (p := h). rewrite Nat.sub_add; auto with Arith. eapply Nat.lt_le_trans; eauto . rewrite Nat.add_comm. apply Nat.add_le_mono_l. apply Nat.nlt_ge in Hha; auto with Arith. apply Nat.nlt_ge in Hcge. apply Nat.le_antisymm; assumption. exfalso. 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 Hna as (Hia, Hna). destruct Hnb as (Hib, Hnb). pose proof (Hnc (na + nb)%nat) as Hnab. unfold convol_mul in Hnab. destruct (le_dec na nb) as [Hab| Hab]. rewrite summation_only_one_non_0 with (v := na) in Hnab. rewrite Nat.add_comm, Nat.add_sub in Hnab. apply fld_eq_mul_0_l in Hnab; try assumption; contradiction. split; [ apply Nat.le_0_l | apply le_plus_l ]. intros i (_, Hiab) Hina. destruct (lt_dec i na) as [Hilt| Hige]. rewrite Hia; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. apply Nat.nlt_ge in Hige. rewrite Hib. rewrite rng_mul_0_r; reflexivity. apply Nat.add_lt_mono_r with (p := i). rewrite Nat.sub_add; auto with Arith. rewrite Nat.add_comm. apply Nat.add_lt_mono_l, Nat_le_neq_lt; auto with Arith. apply Nat.nle_gt in Hab. rewrite summation_only_one_non_0 with (v := na) in Hnab. rewrite Nat.add_comm, Nat.add_sub in Hnab. apply fld_eq_mul_0_l in Hnab; try assumption; contradiction. split; [ apply Nat.le_0_l | apply le_plus_l ]. intros i (_, Hiab) Hina. destruct (lt_dec i na) as [Hilt| Hige]. rewrite Hia; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. apply Nat.nlt_ge in Hige. rewrite Hib; [ rewrite rng_mul_0_r; reflexivity | idtac ]. apply Nat.add_lt_mono_r with (p := i). rewrite Nat.sub_add; auto with Arith. rewrite Nat.add_comm. apply Nat.add_lt_mono_l, Nat_le_neq_lt; auto with Arith. simpl. apply series_series_order_inf_iff in Hnb. rewrite Hnb in Hnc. rewrite rng_mul_0_r in Hnc. simpl in Hnc. rewrite series_order_series_0 in Hnc. subst nc; constructor. simpl. apply series_series_order_inf_iff in Hna. rewrite Hna in Hnc. rewrite rng_mul_0_l in Hnc. simpl in Hnc. rewrite series_order_series_0 in Hnc. subst nc; constructor. 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