add lemma for last line of proof 4

FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean

@@ -13,7 +13,7 @@ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 See the License for the specific language governing permissions and
 limitations under the License.
 
-Authors: Moritz Firsching
+Authors: Moritz Firsching, Ralf Stephan
 -/
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.PrimeCounting
@@ -224,6 +224,33 @@ lemma H_P4_1 {k p: ℝ} (hk: k > 0) (hp: p ≥ k + 1): p / (p - 1) ≤ (k + 1) /
     one_div_le_one_div h_p_pred_pos hk, @le_sub_iff_add_le]
   exact hp
 
+lemma prod_Icc_succ_div (n : ℕ) (hn : 2 ≤ n) : (∏ x in Icc 1 n, ((x + 1) : ℝ) / x) = n + 1 := by
+  induction n with
+  | zero => linarith
+  | succ n ih =>
+    have hnpos : 1 ≤ n := by linarith
+    have hall (hn': n ≥ 1) : ∏ x in Finset.Icc 1 n, ((x + 1) : ℝ) / x = n + 1 := by
+      cases lt_or_eq_of_le hn'
+      case inr heq =>
+        rw [heq.symm]
+        simp only [Finset.Icc_self, prod_div_distrib, Finset.prod_singleton, Nat.cast_one, div_one]
+      case inl hlt => exact ih hlt
+    rw [← mul_prod_Ico_eq_prod_Icc, Nat.cast_succ]
+    rw [add_assoc, one_add_one_eq_two, prod_Ico_succ_top]
+    nth_rewrite 1 [mul_comm]
+    rw [prod_Ico_mul_eq_prod_Icc, hall, mul_div ((n : ℝ) + 1) ((n : ℝ) + 2) ((n : ℝ) + 1)]
+    rw [mul_comm, mul_div_cancel_of_imp]
+    assumption'
+    . intro hl
+      have : ¬((n : ℝ) + 1 = 0) := by linarith
+      contradiction
+    . exact Nat.one_le_of_lt hn
+
+lemma H_P4_2 (hx : x ≥ 3) (hpi3 : (π 3) = 2): (∏ x in Icc 1 (π x), ((x + 1) : ℝ) / x) = (π x) + 1 := by
+  rw [prod_Icc_succ_div]
+  rw [← hpi3]
+  refine Monotone.imp monotone_primeCounting ?h
+  linarith
 
 /-!
 ### Fifth proof