proposition: Theorem in_K_1_m_mul_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_mul_compat_r with (ps₃ := psb) in Hab. rewrite Hb in Hab at 2. unfold ps_mul in Hab at 1. unfold cm, cm_factor in Hab. rewrite Hpa, Hpb in Hab. rewrite <- Z.mul_add_distr_r in Hab. rewrite <- series_stretch_mul in Hab. exists (mkps (ps_terms psa * ps_terms psb) (ps_ordnum psa + ps_ordnum psb) 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. reflexivity. 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