proposition: Lemma clearbit_iff : forall a n m, (clearbit a n).[m] = true <-> a.[m] = true /\ n~=m.
proof: Proof. intros. rewrite clearbit_eqb, andb_true_iff, <- eqb_eq. now rewrite negb_true_iff, not_true_iff_false. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog