Move to OCaml 3.10. Requires debian packages from unstable (soon in testing).

[helm.git] / helm / software / matita / library / algebra / finite_groups.ma

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 79521e20650c95f8a2016df8c0e82ae921a432ad..7f76ae0c852f62c5b88d50818c6821894bb84508 100644 (file)
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -175,11 +175,7 @@ intro;
 apply (not_le_Sn_n ? H3).
 qed.
 
-theorem lt_S_S: ∀n,m. n < m → S n < S m.
-intros;
-unfold lt in H;
-apply (le_S_S ? ? H).
-qed.
+
 
 (* moved to nat/order.ma 
 theorem lt_O_S: ∀n. O < S n.