Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: divides_nat x0 x1.

Apply H0 with divides_int x0 x1.

Assume H1: and (x0 ∈ omega) (x1 ∈ omega).

Apply H1 with (∃ x2 . and (x2 ∈ omega) (mul_nat x0 x2 = x1)) ⟶ divides_int x0 x1.

Assume H2: x0 ∈ omega.

Assume H3: x1 ∈ omega.

Assume H4: ∃ x2 . and (x2 ∈ omega) (mul_nat x0 x2 = x1).

Apply H4 with divides_int x0 x1.

Let x2 of type ι be given.

Assume H5: (λ x3 . and (x3 ∈ omega) (mul_nat x0 x3 = x1)) x2.

Apply H5 with divides_int x0 x1.

Assume H6: x2 ∈ omega.

Assume H7: mul_nat x0 x2 = x1.

Apply and3I with x0 ∈ int, x1 ∈ int, ∃ x3 . and (x3 ∈ int) (mul_SNo x0 x3 = x1) leaving 3 subgoals.

Apply nat_p_int with x0.

Apply omega_nat_p with x0.

The subproof is completed by applying H2.

Apply nat_p_int with x1.

Apply omega_nat_p with x1.

The subproof is completed by applying H3.

Let x3 of type ο be given.

Assume H8: ∀ x4 . and (x4 ∈ int) (mul_SNo x0 x4 = x1) ⟶ x3.

Apply H8 with x2.

Apply andI with x2 ∈ int, mul_SNo x0 x2 = x1 leaving 2 subgoals.

Apply nat_p_int with x2.

Apply omega_nat_p with x2.

The subproof is completed by applying H6.

Apply mul_nat_mul_SNo with x0, x2, λ x4 x5 . x4 = x1 leaving 3 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

■

Proofgold Proof