## Representation of the Fibonacci and Lucas Numbers in Terms of Floor and Ceiling

In the paper we show how to express the Fibonacci numbers and Lucas numbers using the floor and ceiling operations.

In the paper we show how to express the Fibonacci numbers and Lucas numbers using the floor and ceiling operations.

Rough sets, developed by Pawlak [6], are an important tool to describe a situation of incomplete or partially unknown information. One of the algebraic models deals with the pair of the upper and the lower approximation. Although usually the tolerance or the equivalence relation is taken into account when considering a rough set, here we rather concentrate on the model with the pair of two definable sets, hence we are close to the notion of an interval set. In this article, the lattices of rough sets and intervals are formalized. This paper, being essentially the continuation of [3], is also a step towards the formalization of the algebraic theory of rough sets, as in [4] or [9].

We formalized some basic properties of the Möbius function which is defined classically as

as e.g., its multiplicativity. To enable smooth reasoning about the sum of this number-theoretic function, we introduced an underlying many-sorted set indexed by the set of natural numbers. Its elements are just values of the Möbius function.

The second part of the paper is devoted to the notion of the radical of number, i.e. the product of its all prime factors.

The formalization (which is very much like the one developed in Isabelle proof assistant connected with Avigad's formal proof of Prime Number Theorem) was done according to the book [13].