proposition: Theorem wB_div_4: 4 * (wB / 4) = wB.
proof: Proof. unfold base. assert (2 ^ Zpos w_digits = 4 * (2 ^ (Zpos w_digits - 2))). change 4 with (2 ^ 2). rewrite <- Zpower_exp by zarith. f_equal; zarith. rewrite H. rewrite (fun x => (Z.mul_comm 4 (2 ^x))). rewrite Z_div_mult; zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase