Let m, n and k be given.
Assume H1: divides_int m n.
Assume H2: divides_int m k.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume Hn: n ∈ int.
Assume H.
Apply H to the current goal.
Let n' be given.
Assume H.
Apply H to the current goal.
Assume Hn': n' ∈ int.
Assume H3: m * n' = n.
Apply H2 to the current goal.
Assume H.
Apply H to the current goal.
Assume _.
Assume Hk: k ∈ int.
Assume H.
Apply H to the current goal.
Let k' be given.
Assume H.
Apply H to the current goal.
Assume Hk': k' ∈ int.
Assume H4: m * k' = k.
We will prove m ∈ int ∧ n + k ∈ int ∧ ∃l ∈ int, m * l = n + k.
Apply and3I to the current goal.
An exact proof term for the current goal is Hm.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hk.
We use n' + k' to witness the existential quantifier.
Apply andI to the current goal.
We will prove n' + k' ∈ int.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is Hn'.
An exact proof term for the current goal is Hk'.
We will prove m * (n' + k') = n + k.
rewrite the current goal using mul_SNo_distrL m n' k' (int_SNo m Hm) (int_SNo n' Hn') (int_SNo k' Hk') (from left to right).
We will prove m * n' + m * k' = n + k.
Use f_equal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H4.
∎