.. _basics:

Basics
======

This chapter is designed to introduce you to the nuts and
bolts of mathematical reasoning in Lean: calculating,
applying lemmas and theorems,
and reasoning about generic structures.

.. include:: C02_Basics/S01_Calculating.inc
.. include:: C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.inc
.. include:: C02_Basics/S03_Using_Theorems_and_Lemmas.inc
.. include:: C02_Basics/S04_More_on_Order_and_Divisibility.inc
.. include:: C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.inc