Let m, n and d be given.
Assume Hn: n ∈ int.
Assume H1: gcd_reln m (n + - m) d.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume H2: divides_int d m.
Assume H3: divides_int d (n + - m).
Assume H4: ∀d', divides_int d' m → divides_int d' (n + - m) → d' ≤ d.
Apply H2 to the current goal.
Assume H _.
Apply H to the current goal.
Assume _.
Assume Hm: m ∈ int.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We will prove divides_int d m ∧ divides_int d n ∧ ∀d', divides_int d' m → divides_int d' n → d' ≤ d.
Apply and3I to the current goal.
An exact proof term for the current goal is H2.
We will prove divides_int d n.
rewrite the current goal using add_SNo_minus_R2' n m LnS LmS (from right to left).
We will prove divides_int d ((n + - m) + m).
Apply divides_int_add_SNo to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H2.
Let d' be given.
Assume H5: divides_int d' m.
Assume H6: divides_int d' n.
We will prove d' ≤ d.
Apply H4 to the current goal.
An exact proof term for the current goal is H5.
We will prove divides_int d' (n + - m).
Apply divides_int_add_SNo to the current goal.
An exact proof term for the current goal is H6.
Apply divides_int_minus_SNo to the current goal.
An exact proof term for the current goal is H5.
∎