proposition: Lemma log2_shiftl' : forall a n, 0<a -> log2 (a << n) == max 0 (log2 a + n).
proof: Proof. intros a n Ha. rewrite <- shiftr_opp_r, log2_shiftr by trivial. destruct (le_gt_cases 0 (log2 a + n)); [rewrite 2 max_r | rewrite 2 max_l]; rewrite ?sub_opp_r; try order. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog