(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
interpretation "Natural numbers" 'N = nat.
+default "natural numbers" cic:/matita/nat/nat/nat.ind.
+
+alias num (instance 0) = "natural number".
+
definition pred: nat \to nat \def
\lambda n:nat. match n with
[ O \Rightarrow O