proposition: Lemma log2_shiftr : forall a n, 0<a -> log2 (a >> n) == max 0 (log2 a - n).
proof: Proof. intros a n Ha. destruct (le_gt_cases 0 (log2 a - n)) as [H|H]; [rewrite max_r | rewrite max_l]; try order. - apply log2_bits_unique. + now rewrite shiftr_spec, sub_add, bit_log2. + intros m Hm. destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. rewrite shiftr_spec; trivial. apply bits_above_log2; try order. now apply lt_sub_lt_add_r. - rewrite lt_sub_lt_add_r, add_0_l in H. apply log2_nonpos. apply le_lteq; right. apply shiftr_eq_0_iff. right. now split. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog