Use transitivity with and eps_ 0.

An exact proof term for the current goal is eps_ordsucc_half_add 0 nat_0.

An exact proof term for the current goal is eps_0_1.

∎