proposition: Lemma testbit_spec a n : 0<=n -> exists l h, 0<=l<2^n /\ a == l + (a.[n] + 2*h)*2^n.
proof: Proof. intro Hn. exists (a mod 2^n). exists (a / 2^n / 2). split. - apply mod_pos_bound; order_pos. - rewrite add_comm, mul_comm, (add_comm a.[n]). rewrite (div_mod a (2^n)) at 1 by order_nz. do 2 f_equiv. rewrite testbit_spec' by trivial. apply div_mod. order'. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog