Apply nat_ind with λ x0 . ordsucc x0 ∈ mul_nat 2 (ordsucc x0) leaving 2 subgoals.

Apply mul_nat_1R with 2, λ x0 x1 . 1 ∈ x1.

The subproof is completed by applying In_1_2.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ordsucc x0 ∈ mul_nat 2 (ordsucc x0).

Apply mul_nat_SR with 2, ordsucc x0, λ x1 x2 . ordsucc (ordsucc x0) ∈ x2 leaving 2 subgoals.

Apply nat_ordsucc with x0.

The subproof is completed by applying H0.

Claim L2: nat_p (mul_nat 2 (ordsucc x0))

Apply mul_nat_p with 2, ordsucc x0 leaving 2 subgoals.

The subproof is completed by applying nat_2.

Apply nat_ordsucc with x0.

The subproof is completed by applying H0.

Apply add_nat_SL with 1, mul_nat 2 (ordsucc x0), λ x1 x2 . ordsucc (ordsucc x0) ∈ x2 leaving 3 subgoals.

The subproof is completed by applying nat_1.

The subproof is completed by applying L2.

Apply add_nat_SL with 0, mul_nat 2 (ordsucc x0), λ x1 x2 . ordsucc (ordsucc x0) ∈ ordsucc x2 leaving 3 subgoals.

The subproof is completed by applying nat_0.

The subproof is completed by applying L2.

Apply add_nat_0L with mul_nat 2 (ordsucc x0), λ x1 x2 . ordsucc (ordsucc x0) ∈ ordsucc (ordsucc x2) leaving 2 subgoals.

The subproof is completed by applying L2.

Apply ordinal_ordsucc_In with ordsucc (mul_nat 2 (ordsucc x0)), ordsucc x0 leaving 2 subgoals.

Apply nat_p_ordinal with ordsucc (mul_nat 2 (ordsucc x0)).

Apply nat_ordsucc with mul_nat 2 (ordsucc x0).

The subproof is completed by applying L2.

Apply ordsuccI1 with mul_nat 2 (ordsucc x0), ordsucc x0.

The subproof is completed by applying H1.

■

Proofgold Proof