fact: Definition testbit a n := match n with | 0 => odd a | pos p => match a with | 0 => false | pos a => Pos.testbit a (N.pos p) | neg a => negb (N.testbit (Pos.pred_N a) (N.pos p)) end | neg _ => false end.
imports: BinNums BinPos BinNat