- oCic2NCic and nCic2OCic moved to ng_library

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

diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma
index dd5f37c3610e742ebc71a7224c23482bb7452d8c..129336d8e70fc15ac9d61f24d27cd5da6ccba153 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev_thm.ma
+++ b/helm/software/matita/library/nat/chebyshev_thm.ma
@@ -77,7 +77,7 @@ cut (\forall m.pi_p (S n) primeb
            [apply (bool_elim ? (leb ((S n1)*(S n1)) m))
               [intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
                  [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
-                    [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
+                    [rewrite > H1;rewrite < assoc_times;reflexivity
                     |rewrite > H;lapply (leb_true_to_le ? ? H2);
                      lapply (le_to_not_lt ? ? Hletin);
                      apply (bool_elim ? (leb (S m) (S n1 * S n1)))