proposition: Theorem in_K_1_m_lap_mul_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_mul in Hc. revert lb c Hlb Hc. induction la as [| a]; intros. rewrite lap_mul_nil_l in Hc. contradiction. destruct lb as [| b]. rewrite lap_mul_nil_r in Hc. contradiction. rewrite lap_mul_cons in Hc. simpl in Hc. destruct Hc as [(Hab, Hc)| Hc]. rewrite <- Hc. apply in_K_1_m_mul_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 in_K_1_m_lap_add_compat with (m := m) in Hc; auto with Arith. intros d Hd. apply in_K_1_m_lap_add_compat with (m := m) in Hd; auto with Arith. intros e He. apply IHla with (lb := [b]); auto with Arith. intros f Hf. apply Hla; right; assumption. intros f Hf. simpl in Hf. destruct Hf as [(Hb, Hbf)| ]; [ idtac | contradiction ]. rewrite <- Hbf. apply Hlb; left. split; [ idtac | reflexivity ]. intros H; apply Hb. apply lap_eq_cons_nil_inv in H. destruct H as (H, _); rewrite H. apply lap_eq_0. intros f Hf. clear Hc Hd. induction lb as [| b']; [ contradiction | idtac ]. rewrite lap_mul_cons in Hf. simpl in Hf. destruct Hf as [(Hab, Habf)| Hf]. rewrite <- Habf. apply in_K_1_m_mul_compat. eapply hd_in_K_1_m. apply ps_lap_forall_forall; eauto . intros g h Hgh Hg. rewrite <- Hgh; assumption. destruct (ps_zerop K b') as [Hb| Hb]. rewrite Hb; apply ps_zero_in_K_1_m. apply Hlb; right; left. split; [ idtac | reflexivity ]. intros H; apply Hb; clear Hb. apply lap_eq_cons_nil_inv in H. destruct H; assumption. rewrite lap_mul_nil_l in Hf. rewrite lap_eq_0, lap_add_nil_r in Hf. apply IHlb; auto with Arith. intros e He. apply Hlb. simpl in He; simpl. destruct He as [(Hbb, He)| He]. left. split; [ idtac | assumption ]. intros H; apply Hbb. apply lap_eq_cons_nil_inv in H. destruct H as (Hb, H). rewrite Hb. apply lap_eq_cons_nil_inv in H. destruct H as (_, H); rewrite H. apply lap_eq_0. right; right; assumption. intros d Hd. simpl in Hd. destruct Hd as [(Hab, Hd)| Hd]. rewrite <- Hd; apply ps_zero_in_K_1_m. apply IHla with (lb := lb); auto with Arith. intros e He. destruct (ps_zerop K e) as [Hf| Hf]. rewrite Hf; apply ps_zero_in_K_1_m. apply Hla; right; assumption. intros e He. destruct (ps_zerop K e) as [Hf| Hf]. rewrite Hf; apply ps_zero_in_K_1_m. apply Hlb; 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