An exact proof term for the current goal is (Zplus_mem_omega n Hn).