proposition: Theorem nat_num_Qnat : ∀ i, nat_num (Qnat i) = i.
proof: Proof. intros i. unfold nat_num, Qnat; simpl. rewrite Nat2Z.id; reflexivity. 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