290 Formalization

5 Integers