test files for blueprint

Author: mo271

FormalBook/Chapter_01.lean

@@ -197,7 +197,8 @@ theorem infinity_of_primes₃:
   · refine' minFac_prime <| Nat.ne_of_gt _
     dsimp [mersenne]
     calc 1 < 2^2 - 1 := by norm_num
-        _  ≤ 2^p - 1 := sub_one_le_sub_one <| pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp)
+        _  ≤ 2^p - 1 := Nat.pred_le_pred <| Nat.pow_le_pow_of_le_right Nat.zero_lt_two <| Nat.Prime.two_le hp
+        --sub_one_le_sub_one <| pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp)
   · have h2q : 2 ≤ q := by
       exact Prime.two_le <| minFac_prime <| Nat.ne_of_gt <| lt_of_succ_lt <|
           Nat.sub_le_sub_right ((pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp))) 1

blueprint/src/content.tex

@@ -4,4 +4,6 @@
 %
 % If you want to split the blueprint content into several files then
 % the current file can be a simple sequence of \input. Otherwise It
-% can start with a \section or \chapter for instance.
+% can start with a \section or \chapter for instance.
+
+\input{chapter/test}