(* *)
(**************************************************************************)
-include "nat/nat.ma".
+include "nat/plus.ma".
+(*
let rec f n :=
match n with
[ O => O
| S m => let rec g x :=
match x with
[ O => f m
- | S q => g q] in g m].
\ No newline at end of file
+ | S q =>
+ let rec h y :=
+ match y with
+ [ O => f m + g q
+ | S w => h w]
+ in
+ h q]
+ in
+ g m].
+*)
+
+let rec f n :=
+ match n with
+ [ O => O
+ | S m => g m
+ ]
+and g m :=
+ match m with
+ [ O => O
+ | S n => f n
+ ].
\ No newline at end of file