proposition: Lemma land_spec a a' n : testbit (land a a') n = (testbit a n) && (testbit a' n).
proof: Proof. destruct a, a'; simpl; trivial. - now rewrite andb_false_r. - apply pos_land_spec. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties