title: Division in prolog
body: <p>I'm trying to define the division in prolog using the remainder theorem and the well-ordering principle.</p>
  
  <p>I've got thus far:</p>
  
  <pre><code>less(0, s(0)).
  
  less(0, s(B)) :- less(0, B).
  less(s(A), s(s(B))) :- less(A, s(B)).
  
  add(A,0,A)       :- nat(A).
  add(A,s(B),s(C)) :- add(A,B,C).  % add(A,B+1,C+1) = add(A,B,C)
  
  add2(A,0,A).
  add2(A,s(B),s(C)) :- add2(A,B,C).  % add(A,B+1,C+1) = add(A,B,C)
  
  times(A,0,0).
  times(A,s(B),X) :- times(A,B,X1),
                 add(A,X1,X).
  
  eq(0,0).
  eq(s(A), s(B)) :- eq(A, B).
  
  % A / B = Q (R) =&gt; A = B * Q + R
  div(A, B, Q, R) :- less(R, B), eq(A, add(times(Q, R), R)).
  </code></pre>
  
  <p>But the definition of <code>div</code> is somehow wrong. Could someone please give me a hint?</p>
  
  <p>PS: I shouldn't be using <code>eq</code>, but I couldn't get <code>is</code> or <code>=</code> to work.</p>