for n, k being Nat st n <= k holds
dyadic n c= dyadic k