proposition: Lemma shiftr_eq_0_iff : forall a n, a >> n == 0 <-> a==0 \/ (0<a /\ log2 a < n).
proof: Proof. intros a n. rewrite shiftr_div_pow2, div_small_iff by order_nz. destruct (eq_0_gt_0_cases a) as [EQ|LT]. - rewrite EQ. split. { now left. } intros _. assert (H : 2~=0) by order'. generalize (pow_nonzero 2 n H) (le_0_l (2^n)); order. - rewrite log2_lt_pow2; trivial. split. { right; split; trivial. } intros [H|[_ H]]; now order. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog