Proving $∀x (x ≠ 0 → gcd(x, 0) = x)$ formally attempt

Question

I have proved $a≤gcd(a,0)$ in my attempt to prove $∀x (x ≠ 0 → gcd(x, 0) = x)$ but I am having trouble proving $gcd(a,0)≤a$ see below:

I have access to the normal rules of natural deduction and the following axioms, useful theorems and conjectures:

NOTE: Ignore the last conjecture I am trying to prove that one...

I figured it out here is my completed proof:

Answer 1

Use induction to prove:

$\forall x (x \not = 0 \rightarrow \exists y \: x = s(y))$ ('every non-zero number has a predecessor')

Also, you have as part of an axiom that $gcd(a,0)|a$, meaning that $a = c * gcd(a,0)$ for some $c$, and since $a \not = 0$, you can easily show that $c \not = 0$

So then use the above 'predecessor' theorem to show that $c = s(b)$ for some $b$, and thus:

$a = s(b) * gcd(a,0) = gcd(a,0) * s(b)$

By the Peano axiom that $\forall x \forall y \: x*s(y) = (x*y) + x$ you then get:

$a = (gcd(a,0) * b) + gcd(a,0)$, and that means that:

$gcd(a,0) \le a$