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