proposition: Theorem no_prime_imp_spec_inegality : forall n : nat, power 2 7 <= n -> (forall p : nat, n < p -> p < 2 * n -> ~ prime p) -> power 4 n < power (2 * n) (div (sqr (2 * n)) 2) * power 4 (div (2 * n) 3).
proof: Proof. intros n H H0. apply Nat.le_lt_trans with (2 * n * binomial (2 * n) n). replace 4 with (power 2 2); auto with arith. rewrite power_power; apply binomial_even; auto with arith. apply Nat.lt_le_trans with (2 := H); auto with arith; simpl in |- *; auto with arith. rewrite <- (Nat.sub_add 1 (div (sqr (2 * n)) 2)). rewrite Nat.add_comm. rewrite <- power_mult; rewrite power_SO. rewrite <- (Nat.mul_assoc (2 * n)). apply mult_lt_bis; auto with arith. apply Nat.lt_le_trans with (2 * power 2 7); auto with arith; simpl in |- *; auto with arith. apply upper_bound; auto with arith. apply Nat.lt_succ_r. apply lt_mult_right_anti with (z := 2). apply Nat.lt_trans with (sqr (2 * n)). apply Nat.succ_lt_mono; apply mult_id_lt_inv; auto with arith. apply Nat.le_lt_trans with (2 * n). apply Nat.le_trans with (2 * power 2 3); auto with arith. simpl in |- *; repeat apply le_n_S; auto with arith. apply Nat.le_trans with (2 * power 2 7); auto with arith. apply le_mult; auto with arith. apply power_le_mono; auto with arith. apply sqr_lt. change (sqr (2 * n) < 2 * (1 + div (sqr (2 * n)) 2)); apply div_lt; auto with arith. Qed.
imports: Coq(Wf_nat Ranalysis Rtrigo ArithRing Lra)