Let a be given.

Assume Ha.

Let b be given.

Assume Hb.

Assume H1.

Apply real_complete1 a Ha b Hb to the current goal.

Let n be given.

Assume Hn.

We will prove a n ≤ b n ∧ a n ≤ a (ordsucc n) ∧ b (ordsucc n) ≤ b n.

We prove the intermediate claim L1: ordsucc n = n + 1.

rewrite the current goal using add_nat_add_SNo n Hn 1 (nat_p_omega 1 nat_1) (from right to left).

We will prove ordsucc n = add_nat n 1.

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

We will prove ordsucc n = ordsucc (add_nat n 0).

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

Use reflexivity.

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

An exact proof term for the current goal is H1 n Hn.

∎