An exact proof term for the current goal is neq_i_sym 0 (ordsucc a) (neq_0_ordsucc a).