proposition: Lemma bit_or_split i : i = (i>>1)<<1 lor bit i 0.
proof: Proof. apply bit_ext. intros n; rewrite lor_spec. rewrite bit_lsl, bit_lsr, bit_b2i. case (to_Z_bounded n); intros Hi _. case (Zle_lt_or_eq _ _ Hi). 2: replace 0%Z with [|0|]; auto; rewrite to_Z_eq. 2: intros H; rewrite <-H. 2: replace (0 <? 1) with true; auto. intros H; clear Hi. case_eq (n =? 0). rewrite eqb_spec; intros H1; generalize H; rewrite H1; discriminate. intros _; rewrite orb_false_r. case_eq (n <? 1). rewrite ltb_spec, to_Z_1; intros HH; contradict HH; auto with zarith. intros _. generalize (@bit_M i n); case (_ <=? _). intros H1; rewrite H1; auto. intros _. case (to_Z_bounded n); intros H1n H2n. assert (F1: [|n - 1|] = ([|n|] - 1)%Z). rewrite sub_spec, Zmod_small; rewrite to_Z_1; auto with zarith. generalize (add_le_r 1 (n - 1)); case (_ <=? _); rewrite F1, to_Z_1; intros HH. replace (1 + (n -1)) with n. change (bit i n = bit i n). reflexivity. apply to_Z_inj; rewrite add_spec, F1, Zmod_small; rewrite to_Z_1; auto with zarith. rewrite bit_M; auto; rewrite leb_spec. replace [|n|] with wB; try discriminate; auto with zarith. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz