-theorem lt_O_to_le_teta_exp_teta: ∀m. O < m→
- teta (S(2*m)) < exp 2 (2*m)*teta (S m).
-#m #posm @(le_to_lt_to_lt ? (M m*teta (S m)))
- [@le_teta_M_teta
- |@monotonic_lt_times_l [@lt_O_teta|@lt_M //]
+theorem lt_O_to_le_theta_exp_theta: ∀m. O < m→
+ theta (S(2*m)) < exp 2 (2*m)*theta (S m).
+#m #posm @(le_to_lt_to_lt ? (M m*theta (S m)))
+ [@le_theta_M_theta
+ |@monotonic_lt_times_l [@lt_O_theta|@lt_M //]