@dpiponi Most(?) people are only introduced to the formal "Euclid's division lemma" framing of division (with a unique quotient and remainder) at third level. But it's possible to express that in Prolog as well. quotRem(N, D, Q, R) :- leq(D, N), leq(Q, N), mul(D, Q, P), add(P, R, N), lt(R, D). The symmetry of D and Q here feels like it has something to do with the 'partitive' vs 'quotative' interpretations of division, but maybe that's meaningless nonsense.