Coq < Fixpoint pinus [n:nat] : nat -> nat :=
Coq < [m:nat]Cases n of
Coq <  O => O
Coq < |(S  k) => [k:nat] Cases m of
Coq <  O => (S k)
Coq < |(S l) => [l:nat](pinus k l) end
Coq < end.
