We will prove eps_ 0 * 2 ^ 0 = 1.

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

rewrite the current goal using exp_SNo_nat_0 2 SNo_2 (from left to right).

We will prove 1 * 1 = 1.

An exact proof term for the current goal is mul_SNo_oneR 1 SNo_1.

Let n be given.

Assume Hn.

Assume IHn: eps_ n * 2 ^ n = 1.

We will prove eps_ (ordsucc n) * 2 ^ (ordsucc n) = 1.

rewrite the current goal using exp_SNo_nat_S 2 SNo_2 n Hn (from left to right).

We will prove eps_ (ordsucc n) * (2 * 2 ^ n) = 1.

We prove the intermediate claim LeSn: SNo (eps_ (ordsucc n)).

An exact proof term for the current goal is SNo_eps_ (ordsucc n) (nat_p_omega (ordsucc n) (nat_ordsucc n Hn)).

rewrite the current goal using mul_SNo_assoc (eps_ (ordsucc n)) 2 (2 ^ n) LeSn SNo_2 (SNo_exp_SNo_nat 2 SNo_2 n Hn) (from left to right).

We will prove (eps_ (ordsucc n) * 2) * 2 ^ n = 1.

rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.

We will prove (eps_ (ordsucc n) * (1 + 1)) * 2 ^ n = 1.

rewrite the current goal using mul_SNo_distrL (eps_ (ordsucc n)) 1 1 LeSn SNo_1 SNo_1 (from left to right).

We will prove ((eps_ (ordsucc n) * 1) + (eps_ (ordsucc n) * 1)) * 2 ^ n = 1.

rewrite the current goal using mul_SNo_oneR (eps_ (ordsucc n)) LeSn (from left to right).

We will prove (eps_ (ordsucc n) + eps_ (ordsucc n)) * 2 ^ n = 1.

rewrite the current goal using eps_ordsucc_half_add n Hn (from left to right).

We will prove eps_ n * 2 ^ n = 1.

An exact proof term for the current goal is IHn.