fact: Fixpoint testbit_nat (p:positive) : nat -> bool := match p with | 1 => fun n => match n with | O => true | S _ => false end | p~0 => fun n => match n with | O => false | S n' => testbit_nat p n' end | p~1 => fun n => match n with | O => true | S n' => testbit_nat p n' end end.
imports: BinNums