Attempt to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers I am attempting to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers, but am having a little difficulty and am hoping someone can help.
I have access to the standard rules of natural deduction, the following axioms:

and the following useful formulas:


Here is my attempt so far:


The key formula you will have to use is:
$\forall x \forall y \forall z (z \not = 0 \rightarrow (x\cdot z \le y\cdot z \rightarrow x \le y))$
So, you will need to first consider the special case where $a=0$, but in that case you can easily show that it must be the case that $a1=0$ and $a2=0$, and it is also easy to show that $0|0-0$ so you're done.
So then you can consider $a \not = 0$, and s0 you have:


*

*$a \not = 0$

*$a|a1$

*$a|a2$

*$a1 \le a2$

*$a1 = a3\cdot a$

*$a2 = a4\cdot a$
So then using some = Elim's:


*$a3\cdot a \le a4 \cdot a$ 


And now you use the key formula to get:


*$a3\cdot a \le a4 \cdot a \rightarrow a3 \le a4$

*$a3 \le a4$  (6,7)
and you already have the rest.
