Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: divides_int x0 x1.

Apply H0 with div_SNo x1 x0 ∈ int.

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

Apply H1 with (∃ x2 . and (x2 ∈ int) (mul_SNo x0 x2 = x1)) ⟶ div_SNo x1 x0 ∈ int.

Assume H2: x0 ∈ int.

Assume H3: x1 ∈ int.

Assume H4: ∃ x2 . and (x2 ∈ int) (mul_SNo x0 x2 = x1).

Apply H4 with div_SNo x1 x0 ∈ int.

Let x2 of type ι be given.

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

Apply H5 with div_SNo x1 x0 ∈ int.

Assume H6: x2 ∈ int.

Assume H7: mul_SNo x0 x2 = x1.

Claim L8: SNo x0

Apply int_SNo with x0.

The subproof is completed by applying H2.

Claim L9: SNo x1

Apply int_SNo with x1.

The subproof is completed by applying H3.

Apply xm with x0 = 0, div_SNo x1 x0 ∈ int leaving 2 subgoals.

Assume H10: x0 = 0.

Apply H10 with λ x3 x4 . div_SNo x1 x4 ∈ int.

Apply div_SNo_0_denum with x1, λ x3 x4 . x4 ∈ int leaving 2 subgoals.

The subproof is completed by applying L9.

Apply Subq_omega_int with 0.

Apply nat_p_omega with 0.

The subproof is completed by applying nat_0.

Assume H10: x0 = 0 ⟶ ∀ x3 : ο . x3.

Apply mul_SNo_nonzero_cancel with x0, div_SNo x1 x0, x2, λ x3 x4 . x4 ∈ int leaving 6 subgoals.

The subproof is completed by applying L8.

The subproof is completed by applying H10.

Apply SNo_div_SNo with x1, x0 leaving 2 subgoals.

The subproof is completed by applying L9.

The subproof is completed by applying L8.

Apply int_SNo with x2.

The subproof is completed by applying H6.

Apply mul_div_SNo_invR with x1, x0, λ x3 x4 . x4 = mul_SNo x0 x2 leaving 4 subgoals.

The subproof is completed by applying L9.

The subproof is completed by applying L8.

The subproof is completed by applying H10.

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

The subproof is completed by applying H7 with λ x4 x5 . x3 x5 x4.

The subproof is completed by applying H6.

■

Proofgold Proof