theorem :: STIRL2_1:11

for n being Nat holds min* n = 0