proposition: Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false.
proof: Proof. intros a n. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). apply andb_false_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog