Covers the properties of real numbers, focusing on the total order and completeness, including the Archimedean property and the concepts of supremum and infimum.
Covers inductive propositions in Coq, focusing on evaluation rules for arithmetic expressions and their applications in defining partial and non-deterministic functions.