proposition: Lemma setbit_eqb : forall a n m, 0<=n -> (setbit a n).[m] = eqb n m || a.[m].
proof: Proof. intros. now rewrite setbit_spec', lor_spec, pow2_bits_eqb, orb_comm. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog