From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 15 Nov 2006 09:09:02 +0000 (+0000)
Subject: lt_O_S moved to nat/orders.ma
X-Git-Tag: 0.4.95@7852~809
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dccfee15d96938072fbdf4004a06e5b59ba876dc;hp=57e4568829db52f1959006041d72036ae9663955;p=helm.git

lt_O_S moved to nat/orders.ma
---

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;