Assume H2: ¬ divides_int p a.

Apply orIR to the current goal.

We will prove divides_int p b.

We prove the intermediate claim L1: gcd_reln p a 1.

We will prove divides_int 1 p ∧ divides_int 1 a ∧ ∀d, divides_int d p → divides_int d a → d ≤ 1.

Apply and3I to the current goal.

An exact proof term for the current goal is divides_int_1 p LpZ.

An exact proof term for the current goal is divides_int_1 a Ha.

Let d be given.

Assume Hdp: divides_int d p.

Assume Hda: divides_int d a.

We will prove d ≤ 1.

Apply Hdp to the current goal.

Assume H _.

Apply H to the current goal.

Assume HdZ: d ∈ int.

Assume _.

We prove the intermediate claim LdS: SNo d.

An exact proof term for the current goal is int_SNo d HdZ.

Apply SNoLtLe_or d 0 LdS SNo_0 to the current goal.

Assume H3: d < 0.

We will prove d ≤ 1.

Apply SNoLtLe to the current goal.

We will prove d < 1.

Apply SNoLt_tra d 0 1 LdS SNo_0 SNo_1 to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is SNoLt_0_1.

Assume H3: 0 ≤ d.

We prove the intermediate claim LdN: d ∈ ω.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nonneg_int_nat_p d HdZ H3.

We prove the intermediate claim Ldp: divides_nat d p.

Apply divides_int_divides_nat to the current goal.

We will prove d ∈ ω.

An exact proof term for the current goal is LdN.

We will prove p ∈ ω.

An exact proof term for the current goal is Hp1.

An exact proof term for the current goal is Hdp.

Apply Hp3 d LdN Ldp to the current goal.

Assume H4: d = 1.

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

Apply SNoLe_ref to the current goal.

Assume H4: d = p.

Apply H2 to the current goal.

We will prove divides_int p a.

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

We will prove divides_int d a.

An exact proof term for the current goal is Hda.

We prove the intermediate claim L2: ¬ (p = 0 ∧ a = 0).

Assume H3.

Apply H3 to the current goal.

Assume H4: p = 0.

Assume _.

Apply In_no2cycle 0 1 In_0_1 to the current goal.

We will prove 1 ∈ 0.

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

We will prove 1 ∈ p.

An exact proof term for the current goal is Hp2.

Apply BezoutThm p LpZ a Ha L2 1 to the current goal.

Assume HBezout1: gcd_reln p a 1 → int_lin_comb p a 1 ∧ 0 < 1 ∧ ∀d, int_lin_comb p a d → 0 < d → 1 ≤ d.

Assume _.

Apply HBezout1 L1 to the current goal.

Assume H.

Apply H to the current goal.

Assume H3: int_lin_comb p a 1.

Assume _.

Assume H4: ∀d, int_lin_comb p a d → 0 < d → 1 ≤ d.

Apply int_lin_comb_E4 p a 1 H3 to the current goal.

Let m be given.

Assume Hm: m ∈ int.

Let n be given.

Assume Hn: n ∈ int.

Assume H5: m * p + n * a = 1.

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 L3: b * m * p + b * n * a = b.

rewrite the current goal using mul_SNo_distrL b (m * p) (n * a) LbS (SNo_mul_SNo m p (int_SNo m Hm) (int_SNo p LpZ)) (SNo_mul_SNo n a LnS LaS) (from right to left).

We will prove b * (m * p + n * a) = b.

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

An exact proof term for the current goal is mul_SNo_oneR b LbS.

We will prove divides_int p b.

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

We will prove divides_int p (b * m * p + b * n * a).

Apply divides_int_add_SNo to the current goal.

We will prove divides_int p (b * m * p).

Apply divides_int_mul_SNo_R p (m * p) b Hb to the current goal.

We will prove divides_int p (m * p).

Apply divides_int_mul_SNo_R p p m Hm to the current goal.

We will prove divides_int p p.

An exact proof term for the current goal is divides_int_ref p LpZ.

We will prove divides_int p (b * n * a).

rewrite the current goal using mul_SNo_rotate_3_1 n a b LnS LaS LbS (from right to left).

We will prove divides_int p (n * a * b).

Apply divides_int_mul_SNo_R p (a * b) n Hn to the current goal.

We will prove divides_int p (a * b).

An exact proof term for the current goal is H1.