proposition: Lemma setbit_neq : forall a n m, n~=m -> (setbit a n).[m] = a.[m].
proof: Proof. intros a n m H. rewrite setbit_eqb. rewrite <- eqb_eq in H. apply not_true_is_false in H. now rewrite H. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog