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. hammer. Restart. hfcrush use: BinNat.N.setbit_iff. Qed.
imports: Hammer(Hammer) Arith List