proposition: Lemma clearbit_eqb : forall a n m, (clearbit a n).[m] = a.[m] && negb (eqb n m).
proof: Proof. intros a n m. destruct (le_gt_cases 0 m); [| now rewrite 2 testbit_neg_r]. rewrite clearbit_spec', ldiff_spec. f_equal. f_equal. destruct (le_gt_cases 0 n) as [Hn|Hn]. - now apply pow2_bits_eqb. - symmetry. rewrite pow_neg_r, bits_0, <- not_true_iff_false, eqb_eq; order. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog