Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: divides_int x0 x2.

Assume H1: divides_int x1 x3.

Apply H0 with divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Assume H2: and (x0 ∈ int) (x2 ∈ int).

Apply H2 with (∃ x4 . and (x4 ∈ int) (mul_SNo x0 x4 = x2)) ⟶ divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Assume H3: x0 ∈ int.

Assume H4: x2 ∈ int.

Assume H5: ∃ x4 . and (x4 ∈ int) (mul_SNo x0 x4 = x2).

Apply H5 with divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Let x4 of type ι be given.

Assume H6: (λ x5 . and (x5 ∈ int) (mul_SNo x0 x5 = x2)) x4.

Apply H6 with divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Assume H7: x4 ∈ int.

Assume H8: mul_SNo x0 x4 = x2.

Apply H1 with divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Assume H9: and (x1 ∈ int) (x3 ∈ int).

Apply H9 with (∃ x5 . and (x5 ∈ int) (mul_SNo x1 x5 = x3)) ⟶ divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Assume H10: x1 ∈ int.

Assume H11: x3 ∈ int.

Assume H12: ∃ x5 . and (x5 ∈ int) (mul_SNo x1 x5 = x3).

Apply H12 with divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Let x5 of type ι be given.

Assume H13: (λ x6 . and (x6 ∈ int) (mul_SNo x1 x6 = x3)) x5.

Apply H13 with divides_int (mul_SNo x0 x1) (mul_SNo x2 x3).

Assume H14: x5 ∈ int.

Assume H15: mul_SNo x1 x5 = x3.

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

Apply int_mul_SNo with x0, x1 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H10.

Apply int_mul_SNo with x2, x3 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H11.

Let x6 of type ο be given.

Assume H16: ∀ x7 . and (x7 ∈ int) (mul_SNo (mul_SNo x0 x1) x7 = mul_SNo x2 x3) ⟶ x6.

Apply H16 with mul_SNo x4 x5.

Apply andI with mul_SNo x4 x5 ∈ int, mul_SNo (mul_SNo x0 x1) (mul_SNo x4 x5) = mul_SNo x2 x3 leaving 2 subgoals.

Apply int_mul_SNo with x4, x5 leaving 2 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H14.

Apply mul_SNo_com_4_inner_mid with x0, x1, x4, x5, λ x7 x8 . x8 = mul_SNo x2 x3 leaving 5 subgoals.

Apply int_SNo with x0.

The subproof is completed by applying H3.

Apply int_SNo with x1.

The subproof is completed by applying H10.

Apply int_SNo with x4.

The subproof is completed by applying H7.

Apply int_SNo with x5.

The subproof is completed by applying H14.

set y7 to be ...

set y8 to be ...

Claim L17: ...

...

Let x9 of type ι → ι → ο be given.

Apply L17 with λ x10 . x9 x10 y8 ⟶ x9 y8 x10.

Assume H18: x9 y8 y8.

...

■

Proofgold Proof