Let a be given.
Assume Ha.
Let b be given.
Assume Hb.
Assume H1: ¬ (a = 0 ∧ b = 0).
Let d be given.
Apply iffI to the current goal.
Assume H3: gcd_reln a b d.
We will prove int_lin_comb a b d ∧ 0 < d ∧ ∀d', int_lin_comb a b d' → 0 < d' → d ≤ d'.
Apply least_pos_int_lin_comb_ex a Ha b Hb H1 to the current goal.
Let d' be given.
Assume Hd': int_lin_comb a b d' ∧ 0 < d' ∧ ∀c, int_lin_comb a b c → 0 < c → d' ≤ c.
Apply Hd' to the current goal.
Assume H.
Apply H to the current goal.
Assume Hd'1: int_lin_comb a b d'.
Assume Hd'2: 0 < d'.
Assume Hd'3: ∀c, int_lin_comb a b c → 0 < c → d' ≤ c.
We prove the intermediate claim Ld'g: gcd_reln a b d'.
An exact proof term for the current goal is least_pos_int_lin_comb_gcd a b d' Hd'1 Hd'2 Hd'3.
We prove the intermediate claim Ldd': d = d'.
An exact proof term for the current goal is gcd_reln_uniq a b d d' H3 Ld'g.
rewrite the current goal using Ldd' (from left to right).
An exact proof term for the current goal is Hd'.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hd1: int_lin_comb a b d.
Assume Hd2: 0 < d.
Assume Hd3: ∀d', int_lin_comb a b d' → 0 < d' → d ≤ d'.
We will prove gcd_reln a b d.
An exact proof term for the current goal is least_pos_int_lin_comb_gcd a b d Hd1 Hd2 Hd3.
∎