Fixpoint f (0: nat) (l: list nat) : nat :=
 match l with
 | nil => 0
 | h::t => if 0 <? h then f h t
                     else f 0 t
 end.
goal1: h= f 0 t.
goal2: 0<h.