proposition: Theorem nth_γ_n : ∀ f L n Ln jn αjn kn αkn, Ln = nth_ns n f L → ini_pt Ln = (jn, αjn) → fin_pt Ln = (kn, αkn) → nth_γ n f L = (αjn - αkn) / (kn - jn).
proof: Proof. intros f L n Ln jm αjn kn αkn HLn Hini Hfin. revert f L Ln jm αjn kn αkn HLn Hini Hfin. induction n; intros. simpl in HLn; simpl. subst Ln; unfold γ; simpl. rewrite Hini, Hfin; simpl. reflexivity. simpl in HLn; simpl. eapply IHn; eauto . Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM