aux2: THEORY BEGIN b : VAR posnat n : VAR int q: VAR int ndiv(n,b) : {q: int | n = b * q + rem(b)(n)} ndiv_lt: LEMMA ndiv(n,b) <= n/b m: VAR nat JUDGEMENT ndiv(m,b) HAS_TYPE upto(m) END aux2