begin
theorem Th3:
for
n being
Nat st
n > 1 holds
n < (2 * n) -' 1
theorem Th4:
for
n being
Nat st
n > 1 holds
(n -' 2) + 1
= n -' 1
theorem
for
n being
Nat st
n > 1 holds
(((4 * n) * n) - (2 * n)) / (n + 1) > 1
theorem Th6:
for
n being
Nat st
n > 1 holds
((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) !
theorem Th7:
for
n being
Nat holds 2
* (2 - (3 / (n + 1))) < 4
begin