take f = seq_id (id NAT); :: thesis: f is eventually-non-zero
thus f is eventually-non-zero ; :: thesis: verum