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 x1 x2).

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

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

Assume H3: x0 ∈ int.

Assume H4: x1 ∈ int.

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

Apply mul_SNo_oneR 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 x0, 1, x1, x2 leaving 2 subgoals.

The subproof is completed by applying H1.

Apply divides_int_1 with x2.

The subproof is completed by applying H0.

■

Proofgold Proof