From dccfee15d96938072fbdf4004a06e5b59ba876dc Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 15 Nov 2006 09:09:02 +0000
Subject: [PATCH] lt_O_S moved to nat/orders.ma

---
 matita/library/algebra/finite_groups.ma | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma
index 64c65b266..79521e206 100644
--- a/matita/library/algebra/finite_groups.ma
+++ b/matita/library/algebra/finite_groups.ma
@@ -181,12 +181,13 @@ unfold lt in H;
 apply (le_S_S ? ? H).
 qed.
 
+(* moved to nat/order.ma 
 theorem lt_O_S: ∀n. O < S n.
 intro;
 unfold lt;
 apply le_S_S;
 apply le_O_n.
-qed.
+qed. *)
 
 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
 intros;
-- 
2.39.2