proposition: Lemma testbit_false : forall a n, a.[n] = false <-> (a / 2^n) mod 2 == 0.
proof: Proof. intros a n. rewrite <- testbit_spec'; destruct a.[n]; split; simpl; now try order'. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog