proposition: Lemma lxor_spec a a' n : testbit (lxor a a') n = xorb (testbit a n) (testbit a' n).
proof: Proof. destruct a, a'; simpl; trivial. - now destruct Pos.testbit. - apply pos_lxor_spec. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties