proposition: Lemma testbit_spec' a n : a.[n] == (a / 2^n) mod 2.
proof: Proof. revert a. induct n. - 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. destruct b; order'. - intros n IH a. destruct (exists_div2 a) as (a' & b & H). rewrite H at 1. rewrite testbit_succ_r, IH. f_equiv. rewrite pow_succ_r', <- div_div by order_nz. f_equiv. apply div_unique with b; trivial. destruct b; order'. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog