proposition: Theorem hd_in_K_1_m : ∀ a la m, ps_lap_forall (λ b, in_K_1_m b m) [a … la] → in_K_1_m a m.
proof: Proof. intros a la m Hla. destruct (ps_zerop K a) as [Ha| Ha]. rewrite Ha; apply ps_zero_in_K_1_m. eapply ps_lap_forall_forall in Hla; eauto with Arith. intros b c Hbc Hb. rewrite <- Hbc; assumption. left. split; [ idtac | reflexivity ]. intros H1; apply Ha; clear Ha. apply lap_eq_cons_nil_inv in H1. destruct H1; 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