proposition: Lemma spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
proof: Proof. intros. unfold testbit. symmetry. rewrite spec_odd, spec_shiftr. apply Z.testbit_odd. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen