proposition: Lemma setbit_iff : forall m a n : BinNums.N, n = m \/ true = BinNat.N.testbit a m <-> BinNat.N.testbit (BinNat.N.setbit a n) m = true.
proof: Proof. scrush using (@NArith.BinNat.N.setbit_iff). Qed.
imports: Hammer(Tactics) Arith ZArith