proposition: Lemma shiftr_eq_0_iff : forall a n, a >> n == 0 <-> a==0 \/ (0<a /\ log2 a < n).
proof: Proof. intros a n. destruct (le_gt_cases 0 n) as [Hn|Hn]. - rewrite shiftr_div_pow2, div_small_iff by order_nz. destruct (lt_trichotomy a 0) as [LT|[EQ|LT]]. + split. * intros [(H,_)|(H,H')]. { order. } generalize (pow_nonneg 2 n le_0_2); order. * intros [H|(H,H')]; order. + rewrite EQ. split. * now left. * intros _; left. split; order_pos. + split. * { intros [(H,H')|(H,H')]; right. - split; trivial. apply log2_lt_pow2; trivial. - generalize (pow_nonneg 2 n le_0_2); order. } * intros [H|(H,H')]. { order. } left. split. { order. } now apply log2_lt_pow2. - rewrite shiftr_mul_pow2 by order. rewrite eq_mul_0. split; intros [H|H]. + now left. + elim (pow_nonzero 2 (-n)); try apply opp_nonneg_nonpos; order'. + now left. + destruct H. generalize (log2_nonneg a); order. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog