proposition: Theorem in_K_1_m_lap_mul_r_compat : ∀ a m n, in_K_1_m a m → in_K_1_m a (m * n).
proof: Proof. intros a m n Ha. constructor. inversion_clear Ha. destruct H as (ps, (Hps, Hm)). exists (adjust_ps 0 n ps). split; [ idtac | simpl; rewrite Hm; reflexivity ]. rewrite ps_adjust_eq with (n := O) (k := n) in Hps. assumption. 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