Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: divides_nat x0 x1.

Apply H0 with divides_int_alt1 x0 x1.

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

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

Assume H2: x0 ∈ omega.

Assume H3: x1 ∈ omega.

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

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

Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with x0.

The subproof is completed by applying H2.

Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with x1.

The subproof is completed by applying H3.

Apply H4 with ∃ x2 . and (x2 ∈ int_alt1) (mul_SNo x0 x2 = x1).

Let x2 of type ι be given.

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

Apply H5 with ∃ x3 . and (x3 ∈ int_alt1) (mul_SNo x0 x3 = x1).

Assume H6: x2 ∈ omega.

Assume H7: mul_nat x0 x2 = x1.

Let x3 of type ο be given.

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

Apply H8 with x2.

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

Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 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