- oCic2NCic and nCic2OCic moved to ng_library

[helm.git] / helm / software / matita / library / nat / bertrand.ma

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index 17f4c72e0078ded8e054dc4e750e26aa6b876ea5..ce92ee4edc9d7015079831ff14314ae9c1f90aeb 100644 (file)
--- a/helm/software/matita/library/nat/bertrand.ma
+++ b/helm/software/matita/library/nat/bertrand.ma
@@ -610,7 +610,7 @@ qed.
         
 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
 B_split1 (2*n) \le teta (2 * n / 3).
-intros.unfold B_split1.unfold teta.
+intros. unfold B_split1.unfold teta.
 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
   [apply le_pi_p.intros.
    apply le_exp