proposition: Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false.
proof: Proof. intros a n m ?. destruct (le_gt_cases 0 n). - rewrite mul_pow2_bits by trivial. apply testbit_neg_r. now apply lt_sub_0. - now rewrite pow_neg_r, mul_0_r, bits_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog