proposition: Theorem in_K_1_m_add_compat : ∀ m a b, in_K_1_m a m → in_K_1_m b m → in_K_1_m (a + b) m.
proof: Proof. intros m a b Ha Hb. inversion_clear Ha. rename H into Ha. inversion_clear Hb. rename H into Hb. destruct Ha as (psa, (Ha, Hpa)). destruct Hb as (psb, (Hb, Hpb)). constructor. remember Ha as Hab; clear HeqHab. eapply ps_add_compat_r with (ps₃ := psb) in Hab. rewrite Hb in Hab at 2. unfold ps_add in Hab at 1. unfold cm in Hab. rewrite Hpa, Hpb in Hab. unfold ps_ordnum_add in Hab. unfold cm_factor in Hab. rewrite Hpa, Hpb in Hab. rewrite Z.mul_min_distr_nonneg_r in Hab; auto with Arith. unfold ps_terms_add in Hab. unfold cm_factor in Hab. rewrite Hpa, Hpb in Hab. rewrite Z.mul_min_distr_nonneg_r in Hab; auto with Arith. rewrite Z.mul_min_distr_nonneg_r in Hab; auto with Arith. rewrite <- Z.mul_sub_distr_r in Hab. rewrite <- Z.mul_sub_distr_r in Hab. remember (ps_ordnum psa) as oa. remember (ps_ordnum psb) as ob. remember (ps_terms psa) as sa. remember (ps_terms psb) as sb. remember (oa - Z.min oa ob)%Z as omab. remember (ob - Z.min ob oa)%Z as omba. exists (mkps (adjust_series (Z.to_nat omab) 1 sa + adjust_series (Z.to_nat omba) 1 sb) (Z.min oa ob) m). split; auto with Arith. rewrite <- Hab. rewrite ps_adjust_eq with (n := O) (k := m). unfold adjust_ps; simpl. rewrite Z.sub_0_r. rewrite series_shift_0. apply mkps_morphism; auto with Arith. unfold adjust_series; simpl. rewrite Z2Nat.inj_mul; simpl; auto with Arith. rewrite Z2Nat.inj_mul; simpl; auto with Arith. rewrite <- stretch_shift_series_distr. rewrite <- stretch_shift_series_distr. rewrite <- series_stretch_add_distr. do 2 rewrite series_stretch_1. reflexivity. subst omba. rewrite <- Z.sub_max_distr_l, Z.sub_diag. apply Z.le_max_l. subst omab. rewrite <- Z.sub_max_distr_l, Z.sub_diag. apply Z.le_max_l. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fpolynomial Newton Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base AlgCloCharPol PosOrder CharactPolyn ConvexHull PolyConvexHull F1Eq QbarM