Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: x1 ∈ int.

Assume H1: divides_int x0 x2.

Apply H1 with divides_int x0 (mul_SNo x1 x2).

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

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

Assume H3: x0 ∈ int.

Assume H4: x2 ∈ int.

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

Apply mul_SNo_oneL with x0, λ x3 x4 . divides_int x3 (mul_SNo x1 x2) leaving 2 subgoals.

Apply int_SNo with x0.

The subproof is completed by applying H3.

Apply divides_int_mul_SNo with 1, x0, x1, x2 leaving 2 subgoals.

Apply divides_int_1 with x1.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof