understand two representations of a binary number (coeff-base-exp form, coeff-base accumulating exp form). think about normalize function. is there a way to define it apart from binary to nat to binary again?