:: deftheorem defines div SCM_COMP:def 6 :
for t1, t2 being bin-term holds t1 div t2 = [0,3] -tree (t1,t2);