proposition: Lemma testbit_spec' a n : 0<=n -> a.[n] == (a / 2^n) mod 2.
proof: Proof. intro Hn. revert a. apply le_ind with (4:=Hn). - solve_proper. - intros a. nzsimpl. destruct (exists_div2 a) as (a' & b & H). rewrite H at 1. rewrite testbit_0_r. apply mod_unique with a'; trivial. left. destruct b; split; simpl; order'. - clear n Hn. intros n Hn IH a. destruct (exists_div2 a) as (a' & b & H). rewrite H at 1. rewrite testbit_succ_r, IH by trivial. f_equiv. rewrite pow_succ_r, <- div_div by order_pos. f_equiv. apply div_unique with b; trivial. left. destruct b; split; simpl; order'. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog