proposition: Lemma sub1_lsr : forall i, i <> 0 -> (i - 1) >> 1 = if bit i 0 then i >> 1 else i >> 1 - 1.
proof: Proof. intro i. rewrite <- to_Z_eq, to_Z_0; intro Hi0. assert (Hi : (0 < to_Z i < wB)%Z). generalize (to_Z_bounded i); lia. clear Hi0. rewrite <- to_Z_eq. rewrite lsr_spec, to_Z_sub_1_0, to_Z_1; [ | lia ]. case_eq (bit i 0); intro Hibit. rewrite lsr_spec, to_Z_1. change (2 ^ 1)%Z with 2%Z. rewrite to_Z_split. rewrite Hibit. rewrite <- Z.add_sub_assoc. change (to_Z true) with 1%Z. replace (1 - 1)%Z with 0%Z by ring. rewrite 2!Z.div_add_l; [ reflexivity | lia | lia ]. rewrite to_Z_sub_1_0. rewrite lsr_spec, to_Z_1. change (2 ^ 1)%Z with 2%Z. rewrite to_Z_split. rewrite Hibit. rewrite <- Z.add_sub_assoc. change (to_Z false) with 0%Z. rewrite 2!Z.div_add_l; [ | lia | lia ]. rewrite <- Z.add_sub_assoc; reflexivity. rewrite lsr_spec. change (2 ^ to_Z 1)%Z with 2%Z. apply Z.div_str_pos. split; [ lia | ]. cut (to_Z i <> 1)%Z; [ lia | ]. change 1%Z with (to_Z 1). rewrite to_Z_eq. intro H; rewrite H in Hibit; discriminate. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz