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 LaS: SNo a.
An exact proof term for the current goal is int_SNo a Ha.
We prove the intermediate claim LbS: SNo b.
An exact proof term for the current goal is int_SNo b Hb.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
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 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.
Apply quotient_remainder_int d Ld1 a Ha to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Assume Hq: q ∈ int.
Assume H.
Apply H to the current goal.
Let r be given.
Assume H.
Apply H to the current goal.
Assume Hr: r ∈ d.
Assume H1: a = q * d + r.
We prove the intermediate claim LqS: SNo q.
Apply int_SNo to the current goal.
An exact proof term for the current goal is Hq.
We prove the intermediate claim LmqS: SNo (- q).
Apply SNo_minus_SNo q LqS to the current goal.
We prove the intermediate claim LrN: nat_p r.
An exact proof term for the current goal is nat_p_trans d LdN r Hr.
We prove the intermediate claim Lrnn: 0 ≤ r.
Apply omega_nonneg to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is LrN.
We prove the intermediate claim Lrd: r < d.
Apply ordinal_In_SNoLt d (nat_p_ordinal d LdN) r Hr to the current goal.
We prove the intermediate claim LqdS: SNo (q * d).
An exact proof term for the current goal is SNo_mul_SNo q d LqS LdS.
We prove the intermediate claim LrS: SNo r.
An exact proof term for the current goal is nat_p_SNo r LrN.
We prove the intermediate claim L1: r = (1 + - q * m) * a + (- q * n) * b.
Use transitivity with a + - q * d, and a + (- q) * (m * a + n * b).
We will prove r = a + - q * d.
rewrite the current goal using add_SNo_com a (- q * d) LaS (SNo_minus_SNo (q * d) LqdS) (from left to right).
We will prove r = - q * d + a.
rewrite the current goal using H1 (from left to right).
We will prove r = - q * d + q * d + r.
Use symmetry.
An exact proof term for the current goal is add_SNo_minus_L2 (q * d) r LqdS LrS.
We will prove a + - q * d = a + (- q) * (m * a + n * b).
Use f_equal.
We will prove - q * d = (- q) * (m * a + n * b).
rewrite the current goal using mul_SNo_minus_distrL q d LqS LdS (from right to left).
We will prove (- q) * d = (- q) * (m * a + n * b).
Use f_equal.
We will prove d = m * a + n * b.
Use symmetry.
An exact proof term for the current goal is H2.
We will prove a + (- q) * (m * a + n * b) = (1 + - q * m) * a + (- q * n) * b.
rewrite the current goal using mul_SNo_distrL (- q) (m * a) (n * b) LmqS (SNo_mul_SNo m a LmS LaS) (SNo_mul_SNo n b LnS LbS) (from left to right).
We will prove a + ((- q) * (m * a)) + ((- q) * (n * b)) = (1 + - q * m) * a + (- q * n) * b.
rewrite the current goal using add_SNo_assoc a ((- q) * (m * a)) ((- q) * (n * b)) LaS (SNo_mul_SNo (- q) (m * a) LmqS (SNo_mul_SNo m a LmS LaS)) (SNo_mul_SNo (- q) (n * b) LmqS (SNo_mul_SNo n b LnS LbS)) (from left to right).
We will prove (a + (- q) * (m * a)) + (- q) * (n * b) = (1 + - q * m) * a + (- q * n) * b.
Use f_equal.
We will prove a + (- q) * (m * a) = (1 + - q * m) * a.
rewrite the current goal using mul_SNo_minus_distrL q m LqS LmS (from right to left).
We will prove a + (- q) * (m * a) = (1 + (- q) * m) * a.
rewrite the current goal using mul_SNo_distrR 1 ((- q) * m) a SNo_1 (SNo_mul_SNo (- q) m LmqS LmS) LaS (from left to right).
We will prove a + (- q) * (m * a) = 1 * a + ((- q) * m) * a.
Use f_equal.
We will prove a = 1 * a.
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneL a LaS.
We will prove (- q) * (m * a) = ((- q) * m) * a.
An exact proof term for the current goal is mul_SNo_assoc (- q) m a LmqS LmS LaS.
We will prove (- q) * (n * b) = (- q * n) * b.
rewrite the current goal using mul_SNo_minus_distrL q n LqS LnS (from right to left).
An exact proof term for the current goal is mul_SNo_assoc (- q) n b LmqS LnS LbS.
We prove the intermediate claim L2: int_lin_comb a b r.
We will prove a ∈ int ∧ b ∈ int ∧ r ∈ int ∧ ∃m n ∈ int, m * a + n * b = r.
Apply and4I to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is LrN.
We will prove ∃m n ∈ int, m * a + n * b = r.
We use (1 + - q * m) to witness the existential quantifier.
Apply andI to the current goal.
We will prove 1 + - q * m ∈ int.
Apply int_add_SNo to the current goal.
Apply Subq_omega_int to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
Apply int_minus_SNo to the current goal.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is Hq.
An exact proof term for the current goal is Hm.
We use (- q * n) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - q * n ∈ int.
Apply int_minus_SNo to the current goal.
Apply int_mul_SNo to the current goal.
An exact proof term for the current goal is Hq.
An exact proof term for the current goal is Hn.
Use symmetry.
An exact proof term for the current goal is L1.
We prove the intermediate claim L3: r = 0.
Apply SNoLeE 0 r SNo_0 LrS Lrnn to the current goal.
Assume H2: 0 < r.
We will prove False.
Apply SNoLt_irref r to the current goal.
We will prove r < r.
Apply SNoLtLe_tra r d r LrS LdS LrS Lrd to the current goal.
We will prove d ≤ r.
Apply Hd3 to the current goal.
We will prove int_lin_comb a b r.
An exact proof term for the current goal is L2.
We will prove 0 < r.
An exact proof term for the current goal is H2.
Assume H2: 0 = r.
Use symmetry.
An exact proof term for the current goal is H2.
We will prove divides_int d a.
We will prove d ∈ int ∧ a ∈ int ∧ ∃k ∈ int, d * k = a.
Apply and3I to the current goal.
An exact proof term for the current goal is HdZ.
An exact proof term for the current goal is Ha.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
We will prove d * q = a.
rewrite the current goal using H1 (from left to right).
We will prove d * q = q * d + r.
rewrite the current goal using L3 (from left to right).
rewrite the current goal using add_SNo_0R (q * d) LqdS (from left to right).
We will prove d * q = q * d.
An exact proof term for the current goal is mul_SNo_com d q LdS LqS.
∎