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. destruct (le_gt_cases 0 m) as [Hm|Hm]; [|now rewrite !testbit_neg_r]. rewrite testbit_eqb; trivial. 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. - rewrite mul_comm, mul_assoc, <- pow_add_r, (add_comm m), sub_add; trivial. + rewrite add_comm, <- div_mod by order_nz. symmetry. apply testbit_eqb; trivial. + apply le_0_sub; order. - now apply lt_le_pred, lt_0_sub. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog