proposition: Lemma clearbit_neq : forall a n m, n~=m -> (clearbit a n).[m] = a.[m].
proof: Proof. intros a n m H. rewrite clearbit_eqb. rewrite <- eqb_eq in H. apply not_true_is_false in H. rewrite H. apply andb_true_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog