proposition: Lemma shiftl_nonneg : forall a n, 0 <= (a << n) <-> 0 <= a.
proof: Proof. intros a n. destruct (le_ge_cases 0 n) as [Hn|Hn]. - rewrite 2 bits_iff_nonneg_ex. split; intros (k,Hk). + exists (k-n). intros m Hm. destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. rewrite <- (add_simpl_r m n), <- (shiftl_spec a n) by order_pos. apply Hk. now apply lt_sub_lt_add_r. + exists (k+n). intros m Hm. destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. rewrite shiftl_spec by trivial. apply Hk. now apply lt_add_lt_sub_r. - rewrite <- shiftr_opp_r, 2 bits_iff_nonneg_ex. split; intros (k,Hk). + destruct (le_gt_cases 0 k). * exists (k-n). intros m Hm. apply lt_sub_lt_add_r in Hm. rewrite <- (add_simpl_r m n), <- add_opp_r, <- (shiftr_spec a (-n)) by order. now apply Hk. * assert (EQ : a >> (-n) == 0). { apply bits_inj'. intros m Hm. rewrite bits_0. apply Hk; order. } apply shiftr_eq_0_iff in EQ. rewrite <- bits_iff_nonneg_ex. destruct EQ as [EQ|[LT _]]; order. + exists (k+n). intros m Hm. destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. rewrite shiftr_spec by trivial. apply Hk. rewrite add_opp_r. now apply lt_add_lt_sub_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog