freescale porting to ng, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / nat.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
index cff29e3c32ad53b176126457446bccd9010bebf7..1b5f5f46a30a200f308bdacc7a512f5a4fc35286 100755 (executable)
--- 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