for n being non zero Nat holds NatDivisors n c= Seg n