proposition: Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p).
proof: Proof. intros x p. unfold testbit. destr_norm_pos p; simpl. destr_norm_pos x; simpl. apply NN.spec_testbit. rewrite NN.spec_testbit, NN.spec_pred, Z.max_r by auto with zarith. symmetry. apply Z.bits_opp. apply NN.spec_pos. symmetry. apply Z.testbit_neg_r; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig