proposition: Lemma log2_shiftl : forall a n, 0<a -> 0<=n -> log2 (a << n) == log2 a + n.
proof: Proof. intros a n Ha Hn. rewrite shiftl_mul_pow2, add_comm by trivial. now apply log2_mul_pow2. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog