for n being non zero Nat holds Absval (Bin1 n) = 1