proposition: Lemma log2_shiftr : forall a n, log2 (a >> n) == log2 a - n.
proof: Proof. intros a n. destruct (eq_0_gt_0_cases a) as [Ha|Ha]. - now rewrite Ha, shiftr_0_l, log2_nonpos, sub_0_l by order. - destruct (lt_ge_cases (log2 a) n). + rewrite shiftr_eq_0, log2_nonpos by order. symmetry. rewrite sub_0_le; order. + apply log2_bits_unique. * now rewrite shiftr_spec', sub_add, bit_log2 by order. * intros m Hm. rewrite shiftr_spec'; trivial. apply bits_above_log2; try order. now apply lt_sub_lt_add_r. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog