proposition: Lemma mod_pow2_bits_low : forall a n m, m<n -> (a mod 2^n).[m] = a.[m].
proof: Proof. intros a n m H. rewrite testbit_eqb. rewrite <- (mod_add _ (2^(P (n-m))*(a/2^n))) by order'. rewrite <- div_add by order_nz. rewrite (mul_comm _ 2), mul_assoc, <- pow_succ_r', succ_pred by now apply sub_gt. rewrite mul_comm, mul_assoc, <- pow_add_r, (add_comm m), sub_add by order. rewrite add_comm, <- div_mod by order_nz. symmetry. apply testbit_eqb. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog