RS_prime_helper.p_n_lower_small

lemma p_n_lower_small (n : ℕ) (hn1 : n > 1) (hn2 : n ≤ 31) :    (nth_prime' n : ℝ) > n * (Real.log n + Real.log (Real.log n) - 3 / 2) := by  interval_cases n  · exact nth_prime_gt_bound 2 3 count_prime_3_le_1 (by interval_auto)  · exact nth_prime_gt_bound 3 5 count_prime_5_le_2 (by interval_auto)  · exact nth_prime_gt_bound 4 7 count_prime_7_le_3 (by interval_auto)  · exact nth_prime_gt_bound 5 11 count_prime_11_le_4 (by interval_auto)  · exact nth_prime_gt_bound 6 13 count_prime_13_le_5 (by interval_auto)  · exact nth_prime_gt_bound 7 17 count_prime_17_le_6 (by interval_auto)  · exact nth_prime_gt_bound 8 19 count_prime_19_le_7 (by interval_auto)  · exact nth_prime_gt_bound 9 23 count_prime_23_le_8 (by interval_auto)  · exact nth_prime_gt_bound 10 29 count_prime_29_le_9 (by interval_auto)  · exact nth_prime_gt_bound 11 31 count_prime_31_le_10 (by interval_auto)  · exact nth_prime_gt_bound 12 37 count_prime_37_le_11 (by interval_auto)  · exact nth_prime_gt_bound 13 41 count_prime_41_le_12 (by interval_auto)  · exact nth_prime_gt_bound 14 43 count_prime_43_le_13 (by interval_auto)  · exact nth_prime_gt_bound 15 47 count_prime_47_le_14 (by interval_auto)  · exact nth_prime_gt_bound 16 53 count_prime_53_le_15 (by interval_auto)  · exact nth_prime_gt_bound 17 59 count_prime_59_le_16 (by interval_auto)  · exact nth_prime_gt_bound 18 61 count_prime_61_le_17 (by interval_auto)  · exact nth_prime_gt_bound 19 67 count_prime_67_le_18 (by interval_auto)  · exact nth_prime_gt_bound 20 71 count_prime_71_le_19 (by interval_auto)  · exact nth_prime_gt_bound 21 73 count_prime_73_le_20 (by interval_auto)  · exact nth_prime_gt_bound 22 79 count_prime_79_le_21 (by interval_auto)  · exact nth_prime_gt_bound 23 83 count_prime_83_le_22 (by interval_auto)  · exact nth_prime_gt_bound 24 89 count_prime_89_le_23 (by interval_auto)  · exact nth_prime_gt_bound 25 97 count_prime_97_le_24 (by interval_auto)  · exact nth_prime_gt_bound 26 101 count_prime_101_le_25 (by interval_auto)  · exact nth_prime_gt_bound 27 103 count_prime_103_le_26 (by interval_auto)  · exact nth_prime_gt_bound 28 107 count_prime_107_le_27 (by interval_auto)  · exact nth_prime_gt_bound 29 109 count_prime_109_le_28 (by interval_auto)  · exact nth_prime_gt_bound 30 113 count_prime_113_le_29 (by interval_auto)  · exact nth_prime_gt_bound 31 127 count_prime_127_le_30 (by interval_auto)