Apply and7I to the current goal.

An exact proof term for the current goal is gcd_id.

An exact proof term for the current goal is gcd_0.

Let m be given.

Assume Hm.

Apply gcd_sym to the current goal.

An exact proof term for the current goal is gcd_0 m Hm.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn Hmn.

Let d be given.

We will prove gcd_reln m (n + - m) d → gcd_reln m n d.

An exact proof term for the current goal is euclidean_algorithm_prop_1 m n d (Subq_omega_int n Hn).

Let m be given.

Assume Hm.

Let n be given.

Assume Hn Hnm.

Let d be given.

We will prove gcd_reln n m d → gcd_reln m n d.

An exact proof term for the current goal is gcd_sym n m d.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn Hnneg.

Let d be given.

We will prove gcd_reln m (- n) d → gcd_reln m n d.

rewrite the current goal using minus_SNo_invol n (int_SNo n Hn) (from right to left) at position 2.

We will prove gcd_reln m (- n) d → gcd_reln m (- - n) d.

An exact proof term for the current goal is gcd_minus m (- n) d.

Let m be given.

Assume Hm.

Let n be given.

Assume Hn Hmneg.

Let d be given.

We will prove gcd_reln (- m) n d → gcd_reln m n d.

Assume H1: gcd_reln (- m) n d.

We will prove gcd_reln m n d.

Apply gcd_sym to the current goal.

We will prove gcd_reln n m d.

rewrite the current goal using minus_SNo_invol m (int_SNo m Hm) (from right to left).

Apply gcd_minus to the current goal.

Apply gcd_sym to the current goal.

An exact proof term for the current goal is H1.

∎