Indeed :-)
    j >= max_j || p (get m i j) || on_j p m i max_j (j+1)
should to the trick. Same for on_i.