proposition: Lemma mul_pow2_bits : forall a n m, 0<=n -> (a*2^n).[m] = a.[m-n].
proof: Proof. intros a n m ?. rewrite <- (add_simpl_r m n) at 1. rewrite add_sub_swap, add_comm. now apply mul_pow2_bits_add. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog