X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fac.ma;h=2d7d320e886ff7858be14ea5674683a6fa4d4ef1;hp=aa9b4db7b306f4de9c5ed89ecc3ea5f7bc2692f3;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma
index aa9b4db7b..2d7d320e8 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/lib/arith.ma".
+include "ground/arith/nat_le.ma".
 include "static_2/notation/functions/one_0.ma".
 include "static_2/notation/functions/two_0.ma".
 include "static_2/notation/functions/omega_0.ma".
@@ -46,13 +46,13 @@ qed.
 definition ac_eq (k): ac ≝ mk_ac (eq … k).
 
 interpretation "one (applicability domain)"
-  'Two = (ac_eq (S O)).
+  'Two = (ac_eq (nsucc nzero)).
 
 interpretation "zero (applicability domain)"
-  'One = (ac_eq O).
+  'One = (ac_eq nzero).
 
 lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props ….
-#m elim (le_dec m k) #Hm
+#m elim (nle_dec m k) #Hm
 [ /3 width=3 by or_introl, ex2_intro/
 | @or_intror * #n #Hn #Hmn destruct /2 width=1 by/
 ]
@@ -61,9 +61,9 @@ qed.
 definition ac_le (k): ac ≝ mk_ac (λn. n ≤ k).
 
 lemma ac_le_props (k): ac_props (ac_le k) ≝ mk_ac_props ….
-#m elim (le_dec m k) #Hm
+#m elim (nle_dec m k) #Hm
 [ /3 width=3 by or_introl, ex2_intro/
 | @or_intror * #n #Hn #Hmn
-  /3 width=3 by transitive_le/
+  /3 width=3 by nle_trans/
 ]
 qed.