fact: Definition testbit a n := match norm_pos n, norm_pos a with | Pos p, Pos a => NN.testbit a p | Pos p, Neg a => negb (NN.testbit (NN.pred a) p) | Neg p, _ => false end.
imports: ZArith Lia BigNumPrelude NSig ZSig