proposition: Lemma lor_spec a a' n : testbit (lor a a') n = (testbit a n) || (testbit a' n).
proof: Proof. destruct a, a'; simpl; trivial. - now rewrite orb_false_r. - apply pos_lor_spec. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties