proposition: Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false.
proof: Proof. intros a n m H. apply testbit_false. rewrite <- (sub_add m n) by order'. rewrite pow_add_r, mul_assoc. rewrite div_mul by order_nz. rewrite <- (succ_pred (n-m)). - rewrite pow_succ_r. + now rewrite (mul_comm 2), mul_assoc, mod_mul by order'. + apply lt_le_pred. apply sub_gt in H. generalize (le_0_l (n-m)); order. - now apply sub_gt. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog