proposition: Lemma setbit_iff : forall a n m, 0<=n -> ((setbit a n).[m] = true <-> n==m \/ a.[m] = true).
proof: Proof. intros. now rewrite setbit_eqb, orb_true_iff, eqb_eq. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog