proposition: Lemma testbit_eqb : forall a n, 0<=n -> a.[n] = eqb ((a / 2^n) mod 2) 1.
proof: Proof. intros a n Hn. apply eq_true_iff_eq. now rewrite testbit_true, eqb_eq. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog