Let a, b and d be given.

Assume H1.

Apply int_lin_comb_E a b d H1 to the current goal.

Assume Ha Hb Hd.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn.

Assume H2: m * a + n * b = d.

Apply int_lin_comb_I b Hb a Ha d Hd to the current goal.

We will prove ∃n m ∈ int, n * b + m * a = d.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hn.

We use m to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hm.

We will prove n * b + m * a = d.

rewrite the current goal using add_SNo_com (n * b) (m * a) (SNo_mul_SNo n b (int_SNo n Hn) (int_SNo b Hb)) (SNo_mul_SNo m a (int_SNo m Hm) (int_SNo a Ha)) (from left to right).

An exact proof term for the current goal is H2.

∎