include "nat/plus.ma".
+(*
let rec f n :=
match n with
[ O => O
in
h q]
in
- g m].
\ No newline at end of file
+ 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