to express that the proof object “\(\divi\)” is a function which maps two numbers \(m\) and \(n\) and a proof-object \(p\) witnessing that \(m &gt; 0\) to a quadruple \((q,(r,(s,t)))\), where \(q\) is the quotient and \(r\) is the remainder obtained when dividing \(n\) by \(m\). The third component \(s\) is a proof-object witnessing the fact that \(mq + r = n\) and the fourth component \(t\) is a proof object witnessing \(m &gt; r \).