proposition: Theorem in_K_1_m_lap_add_compat : ∀ m la lb c, (∀ a, ps_lap_in a la → in_K_1_m a m) → (∀ b, ps_lap_in b lb → in_K_1_m b m) → ps_lap_in c (la + lb) → in_K_1_m c m.
proof: Proof. intros m la lb c Hla Hlb Hc. rewrite <- fold_ps_lap_add in Hc. revert lb Hlb Hc. induction la as [| a]; intros. simpl in Hc. apply Hlb; assumption. destruct lb as [| b]. simpl in Hc. destruct Hc as [(Ha, Hac)| Hc]. rewrite <- Hac. apply Hla; left. split; [ assumption | reflexivity ]. apply Hla; right; assumption. simpl in Hc. destruct Hc as [(Hab, Hac)| Hc]. rewrite <- Hac. apply in_K_1_m_add_compat. eapply hd_in_K_1_m. apply ps_lap_forall_forall; eauto . intros d e Hde Hd. rewrite <- Hde; assumption. eapply hd_in_K_1_m. apply ps_lap_forall_forall; eauto . intros d e Hde Hd. rewrite <- Hde; assumption. apply IHla with (lb := lb). intros d Hd. apply Hla; right; assumption. intros d Hd. apply Hlb; right; assumption. 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