proposition: Lemma setbit_neq : forall a n m, 0<=n -> n~=m -> (setbit a n).[m] = a.[m].
proof: Proof. intros a n m Hn H. rewrite setbit_eqb; trivial. rewrite <- eqb_eq in H. apply not_true_is_false in H. now rewrite H. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog