proposition: Theorem ps_lap_forall_forall : ∀ la (P : puiseux_series α → Prop), (∀ a b, (a = b)%ps → P a → P b) → ps_lap_forall P la ↔ (∀ a, ps_lap_in a la → P a).
proof: Proof. intros la P Hmorph. split; [ intros Hfa a Hin | intros Hfa ]. revert a Hin. induction la as [| b]; intros; [ contradiction | idtac ]. simpl in Hin. destruct Hin as [(Hbla, Hba)| Hin]. inversion_clear Hfa; [ contradiction | idtac ]. eapply Hmorph; eassumption. inversion_clear Hfa. inversion_clear H. rewrite H1 in Hin; contradiction. apply IHla; assumption. induction la as [| b]; [ constructor; reflexivity | idtac ]. destruct (ps_lap_nilp _ [b … la]) as [Hba| Hba]. constructor 1; assumption. constructor 2; [ assumption | idtac | idtac ]. apply Hfa; left. split; [ assumption | reflexivity ]. apply IHla; intros a Ha. apply Hfa; right; 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