theorem :: NUMBER15:22

for n being non zero Nat holds card (divisors (n,4,3)) <= card (divisors (n,4,1))