proposition: Theorem pt_absc_is_nat : ∀ f pts pt, points_of_ps_polynom f = pts → pt ∈ pts → fst pt = Qnat (Z.to_nat (Qnum (fst pt))).
proof: Proof. intros f pts pt Hpts Hαh. unfold points_of_ps_polynom, points_of_ps_lap in Hpts. remember (al f) as cl; clear Heqcl. remember 0%nat as n in Hpts; clear Heqn. unfold points_of_ps_lap_gen in Hpts. unfold qpower_list in Hpts. revert n pts Hpts Hαh. induction cl as [| c]; intros; [ subst pts; contradiction | idtac ]. simpl in Hpts. destruct cl as [| c₁]. simpl in Hpts. destruct (order c); subst pts; [ idtac | contradiction ]. simpl in Hαh. destruct Hαh as [Hαh| ]; [ idtac | contradiction ]. subst pt; simpl. rewrite Nat2Z.id; reflexivity. simpl in Hpts. simpl in IHcl. destruct (order c). subst pts. destruct Hαh as [Hαh| Hαh]. subst pt; simpl. rewrite Nat2Z.id; reflexivity. eapply IHcl; [ reflexivity | eassumption ]. eapply IHcl; eassumption. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base