Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar.