X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fnat.ma;h=1b5f5f46a30a200f308bdacc7a512f5a4fc35286;hb=20fdd66303330e6209059e90b6a98af71ec29567;hp=cff29e3c32ad53b176126457446bccd9010bebf7;hpb=661cf1186c81c15122e0644b679795d2e6b9d389;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
index cff29e3c3..1b5f5f46a 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
@@ -56,6 +56,13 @@ nlet rec eq_nat (n1,n2:nat) on n1 ≝
   | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
   ].
 
+nlet rec le_nat n m ≝ 
+ match n with 
+  [ O ⇒ true
+  | (S p) ⇒ match m with 
+   [ O ⇒ false | (S q) ⇒ le_nat p q ]
+  ].
+
 nlet rec plus (n1,n2:nat) on n1 ≝ 
  match n1 with
   [ O ⇒ n2