proposition: Theorem summation_all_lt : ∀ f n x, let qr := Q_ring in (∀ i : nat, i ≤ n → x < f i) → x * Qnat (S n) < Σ (i = 0, n), f i.
proof: Proof. intros f n x qr Hi. induction n. unfold Qnat, summation; simpl. rewrite rng_add_0_r. rewrite rng_mul_1_r. apply Hi; reflexivity. rewrite summation_split_last; [ simpl | apply Nat.le_0_l ]. rewrite Qnat_succ. apply Qplus_lt_le_compat. apply IHn. intros i Hin; apply Hi. apply Nat.le_le_succ_r; auto. apply Qlt_le_weak. apply Hi; reflexivity. 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