Fixpoint nonzeros (l:natlist) : natlist
  match l with
  | nil => nil
  | h :: t => match h with
              | 0 => nonzeros t
              | _ => h :: nonzeros t
              end
  end.