proposition: Theorem mul_pos_nonneg : ∀ j k c d, (j < k)%nat → Z.of_nat (k - j) = c * Z.of_nat d → 0 <= c.
proof: Proof. intros j k c d Hjk Hc. apply Z.mul_le_mono_pos_r with (p := Z.of_nat d). destruct d. rewrite Z.mul_comm in Hc; simpl in Hc. rewrite <- Nat2Z.inj_0 in Hc. apply Nat2Z.inj in Hc. apply Nat.sub_0_le in Hc. apply Nat.nlt_ge in Hc. exfalso; apply Hc. contradiction. apply Pos2Z.is_pos. rewrite <- Hc; simpl. apply Nat2Z.is_nonneg. 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