Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: x2 ∈ int.

Assume H1: divides_int x0 x1.

Apply H1 with divides_int x0 (mul_SNo x2 x1).

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

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

Assume H3: x0 ∈ int.

Assume H4: x1 ∈ int.

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

Apply mul_SNo_com with x2, x1, λ x3 x4 . divides_int x0 x4 leaving 3 subgoals.

Apply int_SNo with x2.

The subproof is completed by applying H0.

Apply int_SNo with x1.

The subproof is completed by applying H4.

Apply divides_int_mul_SNo_L with x0, x1, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof