Let a, b and d be given.
Assume Hd1: int_lin_comb a b d.
Assume Hd2: 0 < d.
Assume Hd3: ∀c, int_lin_comb a b c → 0 < c → d ≤ c.
Apply int_lin_comb_E a b d Hd1 to the current goal.
Assume Ha: a ∈ int.
Assume Hb: b ∈ int.
Assume HdZ: d ∈ int.
Let m be given.
Assume Hm: m ∈ int.
Let n be given.
Assume Hn: n ∈ int.
Assume H2: m * a + n * b = d.
We prove the intermediate claim LdN: nat_p d.
Apply nonneg_int_nat_p d HdZ to the current goal.
We will prove 0 ≤ d.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hd2.
We prove the intermediate claim Ld1: d ∈ ω ∖ {0}.
Apply setminusI to the current goal.
We will prove d ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is LdN.
Assume H3: d ∈ {0}.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using SingE 0 d H3 (from right to left) at position 2.
An exact proof term for the current goal is Hd2.
We prove the intermediate claim LdS: SNo d.
An exact proof term for the current goal is nat_p_SNo d LdN.
We prove the intermediate claim Lda: divides_int d a.
Apply least_pos_int_lin_comb_divides_int a b d to the current goal.
An exact proof term for the current goal is Hd1.
An exact proof term for the current goal is Hd2.
An exact proof term for the current goal is Hd3.
We prove the intermediate claim Ldb: divides_int d b.
Apply least_pos_int_lin_comb_divides_int b a d to the current goal.
Apply int_lin_comb_sym to the current goal.
An exact proof term for the current goal is Hd1.
An exact proof term for the current goal is Hd2.
Let c be given.
Assume H2: int_lin_comb b a c.
Assume H3: 0 < c.
We will prove d ≤ c.
Apply Hd3 c to the current goal.
We will prove int_lin_comb a b c.
Apply int_lin_comb_sym to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
We will prove divides_int d a ∧ divides_int d b ∧ ∀d', divides_int d' a → divides_int d' b → d' ≤ d.
Apply and3I to the current goal.
An exact proof term for the current goal is Lda.
An exact proof term for the current goal is Ldb.
Let d' be given.
Assume Hd'a: divides_int d' a.
Assume Hd'b: divides_int d' b.
We will prove d' ≤ d.
We prove the intermediate claim Ld'd: divides_int d' d.
rewrite the current goal using H2 (from right to left).
We will prove divides_int d' (m * a + n * b).
Apply divides_int_add_SNo to the current goal.
We will prove divides_int d' (m * a).
Apply divides_int_mul_SNo_R to the current goal.
An exact proof term for the current goal is Hm.
An exact proof term for the current goal is Hd'a.
We will prove divides_int d' (n * b).
Apply divides_int_mul_SNo_R to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hd'b.
Apply divides_int_pos_Le to the current goal.
An exact proof term for the current goal is Ld'd.
An exact proof term for the current goal is Hd2.
∎