290 Formalization

3 Induction