proposition: Lemma pow2_lsr : forall i n, (to_Z i < 2 ^ Z.of_nat (S n))%Z -> (to_Z (i >> 1) < 2 ^ Z.of_nat n)%Z.
proof: Proof. intros i n Hi. rewrite lsr_spec. change (2 ^ to_Z 1)%Z with 2%Z. apply (Zmult_lt_reg_r _ _ 2); [ lia | ]. rewrite Zmult_comm. apply (Z.le_lt_trans _ (to_Z i)). apply Z.mul_div_le; lia. rewrite <- two_power_nat_equiv in *. rewrite two_power_nat_S in Hi. rewrite Zmult_comm; assumption. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz