-theorem le_A_SSO_A: \forall n.
-A((S(S O))*n) \le
- pi_p (S ((S(S O))*n)) primeb (λp:nat.p)*A n.
-unfold A.intros.
-cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
+theorem le_B_exp: \forall n.
+B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+intro.cases n
+ [apply le_n
+ |cases n1
+ [simplify.apply le_S.apply le_S.apply le_n
+ |apply lt_SO_to_le_B_exp.
+ apply le_S_S.apply lt_O_S.
+ ]
+ ]
+qed.
+
+theorem eq_A_SSO_n: \forall n.O < n \to
+A((S(S O))*n) =
+ pi_p (S ((S(S O))*n)) primeb
+ (\lambda p.(pi_p (log p ((S(S O))*n) )
+ (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
+ *A n.
+intro.
+rewrite > eq_A_A'.rewrite > eq_A_A'.
+unfold A'.intros.
+cut (
+ pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
+ = pi_p (S ((S(S O))*n)) primeb
+ (λp:nat.pi_p (log p ((S(S O))*n)) (λi:nat.true) (λi:nat.(p)\sup(bool_to_nat (\lnot (leb (S n) (exp p (S i))))))))