Apply nat_ind with λ x0 . or (even_nat x0) (odd_nat x0) leaving 2 subgoals.

Apply orIL with even_nat 0, odd_nat 0.

The subproof is completed by applying even_nat_0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: or (even_nat x0) (odd_nat x0).

Apply H1 with or (even_nat (ordsucc x0)) (odd_nat (ordsucc x0)) leaving 2 subgoals.

Assume H2: even_nat x0.

Apply orIR with even_nat (ordsucc x0), odd_nat (ordsucc x0).

Apply exactly1of2_E with even_nat x0, even_nat (ordsucc x0), odd_nat (ordsucc x0) leaving 3 subgoals.

Apply even_nat_xor_S with x0.

The subproof is completed by applying H0.

Assume H3: even_nat x0.

Assume H4: not (even_nat (ordsucc x0)).

Apply andI with ordsucc x0 ∈ omega, ∀ x1 . x1 ∈ omega ⟶ ordsucc x0 = mul_nat 2 x1 ⟶ ∀ x2 : ο . x2 leaving 2 subgoals.

Apply omega_ordsucc with x0.

Apply nat_p_omega with x0.

The subproof is completed by applying H0.

Let x1 of type ι be given.

Assume H5: x1 ∈ omega.

Assume H6: ordsucc x0 = mul_nat 2 x1.

Apply H4.

Apply andI with ordsucc x0 ∈ omega, ∃ x2 . and (x2 ∈ omega) (ordsucc x0 = mul_nat 2 x2) leaving 2 subgoals.

Apply omega_ordsucc with x0.

Apply nat_p_omega with x0.

The subproof is completed by applying H0.

Let x2 of type ο be given.

Assume H7: ∀ x3 . and (x3 ∈ omega) (ordsucc x0 = mul_nat 2 x3) ⟶ x2.

Apply H7 with x1.

Apply andI with x1 ∈ omega, ordsucc x0 = mul_nat 2 x1 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

Assume H3: not (even_nat x0).

Apply FalseE with even_nat (ordsucc x0) ⟶ odd_nat (ordsucc x0).

Apply H3.

The subproof is completed by applying H2.

Assume H2: odd_nat x0.

Apply orIL with even_nat (ordsucc x0), odd_nat (ordsucc x0).

Apply exactly1of2_E with even_nat x0, even_nat (ordsucc x0), even_nat (ordsucc x0) leaving 3 subgoals.

Apply even_nat_xor_S with x0.

The subproof is completed by applying H0.

Assume H3: even_nat x0.

Apply FalseE with not (even_nat (ordsucc x0)) ⟶ even_nat (ordsucc x0).

Apply even_nat_not_odd_nat with x0 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H2.

Assume H3: not (even_nat x0).

Assume H4: even_nat (ordsucc x0).

The subproof is completed by applying H4.

■

Proofgold Proof