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: gcd_reln x0 x1 x2.

Apply H0 with gcd_reln x0 x1 x3 ⟶ x2 = x3.

Assume H1: and (divides_int x2 x0) (divides_int x2 x1).

Apply H1 with (∀ x4 . divides_int x4 x0 ⟶ divides_int x4 x1 ⟶ SNoLe x4 x2) ⟶ gcd_reln x0 x1 x3 ⟶ x2 = x3.

Assume H2: divides_int x2 x0.

Assume H3: divides_int x2 x1.

Assume H4: ∀ x4 . divides_int x4 x0 ⟶ divides_int x4 x1 ⟶ SNoLe x4 x2.

Assume H5: gcd_reln x0 x1 x3.

Apply H5 with x2 = x3.

Assume H6: and (divides_int x3 x0) (divides_int x3 x1).

Apply H6 with (∀ x4 . divides_int x4 x0 ⟶ divides_int x4 x1 ⟶ SNoLe x4 x3) ⟶ x2 = x3.

Assume H7: divides_int x3 x0.

Assume H8: divides_int x3 x1.

Assume H9: ∀ x4 . divides_int x4 x0 ⟶ divides_int x4 x1 ⟶ SNoLe x4 x3.

Apply H2 with x2 = x3.

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

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

Apply H10 with x2 = x3.

Assume H12: x2 ∈ int.

Assume H13: x0 ∈ int.

Apply H7 with x2 = x3.

Assume H14: and (x3 ∈ int) (x0 ∈ int).

Assume H15: ∃ x4 . and (x4 ∈ int) (mul_SNo x3 x4 = x0).

Apply H14 with x2 = x3.

Assume H16: x3 ∈ int.

Assume H17: x0 ∈ int.

Apply SNoLe_antisym with x2, x3 leaving 4 subgoals.

Apply int_SNo with x2.

The subproof is completed by applying H12.

Apply int_SNo with x3.

The subproof is completed by applying H16.

Apply H9 with x2 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

Apply H4 with x3 leaving 2 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

■

Proofgold Proof