proposition: Theorem gamma_in_K_1_mq : ∀ L m a c q, q = q_of_m m (γ L) → (a = ps_monom c (γ L))%ps → in_K_1_m a (m * q).
proof: Proof. intros L m a c q Hq Ha. constructor. remember (p_of_m m (γ L)) as p eqn:Hp . pose proof (any_is_p_mq (γ L) m Hp Hq) as Hgp. destruct Hgp as (Hgp, Hg). exists (ps_monom c (p # m * q)); simpl. split; [ idtac | reflexivity ]. rewrite Ha, Hgp. 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