proposition: Theorem exists_pol_ord : ∀ f, ∃ m, m = ps_pol_com_polydo f ∧ pol_in_K_1_m f m.
proof: Proof. intros f. unfold pol_in_K_1_m. remember (ps_pol_com_polydo f) as m eqn:Hm. exists m; split; [ reflexivity | ]. apply ps_lap_forall_forall. intros a b Hab H. rewrite <- Hab; assumption. intros a Ha. unfold ps_pol_com_polydo in Hm. remember (al f) as la; clear Heqla. revert a m Ha Hm. induction la as [| b]; intros; [ contradiction | idtac ]. simpl in Ha. destruct Ha as [(Hbla, Hba)| Ha]. constructor. simpl in Hm. remember (ps_lap_com_polydo la) as m' eqn:Hm' . exists (adjust_ps 0 m' b). split; [ idtac | simpl; rewrite Pos.mul_comm; symmetry; assumption ]. transitivity b; [ idtac | assumption ]. symmetry; apply ps_adjust_eq. subst m; simpl. apply in_K_1_m_lap_mul_r_compat. apply IHla; [ apply Ha | reflexivity ]. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m