Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply H0 with
gcd_reln x1 x0 x2.
Apply H1 with
(∀ x3 . divides_int x3 x0 ⟶ divides_int x3 x1 ⟶ SNoLe x3 x2) ⟶ gcd_reln x1 x0 x2.
Apply and3I with
divides_int x2 x1,
divides_int x2 x0,
∀ x3 . divides_int x3 x1 ⟶ divides_int x3 x0 ⟶ SNoLe x3 x2 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Apply H4 with
x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.