Use symmetry.

We will prove ordsucc 1 = 1 + ordsucc 0.

rewrite the current goal using add_nat_SR 1 0 nat_0 (from left to right).

We will prove ordsucc 1 = ordsucc (1 + 0).

rewrite the current goal using add_nat_0R 1 (from left to right).

An exact proof term for the current goal is (λq H ⇒ H).

∎