Apply Hmn to the current goal.

Let k be given.

Assume H.

Apply H to the current goal.

Assume Hk: k ∈ int.

Assume H1: m * k = n.

Apply binunionE ω {- n|n ∈ ω} k Hk to the current goal.

Assume H2: k ∈ ω.

We use k to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H2.

We will prove mul_nat m k = n.

rewrite the current goal using mul_nat_mul_SNo m Hm k H2 (from left to right).

An exact proof term for the current goal is H1.

Assume H2: k ∈ {- n|n ∈ ω}.

Apply xm (n = 0) to the current goal.

Assume H3: n = 0.

We prove the intermediate claim L0: 0 ∈ ω.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_0.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is L0.

rewrite the current goal using mul_nat_mul_SNo m Hm 0 L0 (from left to right).

rewrite the current goal using H3 (from left to right).

We will prove m * 0 = 0.

rewrite the current goal using mul_nat_mul_SNo m Hm 0 (nat_p_omega 0 nat_0) (from right to left).

Apply mul_nat_0R to the current goal.

Assume H3: n ≠ 0.

We will prove False.

Apply ReplE_impred ω minus_SNo k H2 to the current goal.

Let j be given.

Assume Hj: j ∈ ω.

We will prove k ≠ - j.

Assume H4: k = - j.

We prove the intermediate claim L1: m * (- j) = n.

rewrite the current goal using H4 (from right to left).

An exact proof term for the current goal is H1.

We prove the intermediate claim L2: n = - (m * j).

Use symmetry.

rewrite the current goal using mul_minus_SNo_distrR m j (omega_SNo m Hm) (omega_SNo j Hj) (from right to left).

An exact proof term for the current goal is L1.

Apply H3 to the current goal.

We prove the intermediate claim Lmj: m * j ∈ ω.

Apply mul_SNo_In_omega to the current goal.

An exact proof term for the current goal is Hm.

An exact proof term for the current goal is Hj.

We will prove n = 0.

Apply nonpos_nonneg_0 n Hn (m * j) Lmj L2 to the current goal.

Assume H _.

An exact proof term for the current goal is H.