@misc{COMPLEX3.MIZ,
  AUTHOR = {Ziobro, Rafal},
  TITLE = {Multiplication-related Classes of Complex Numbers},
  ADDRESS1 = {Department of Carbohydrate Technology, University of Agriculture in Krakow},
  DAY = {31},
  MONTH = {May},
  YEAR = {2020},
  KEYWORDS = {complex numbers, multiplication, order},
  MSC2010 = {40-04 03B35},
  ACKNOWLEDGEMENT = {Ad Maiorem Dei Gloriam},
  SUMMARY = {The use of registrations is useful in shortening Mizar
  proofs \cite{caminati2013custom}, \cite{kornilowicz2013rewriting},
  both in terms of formalization time and article space.
  The proposed system of classes for complex numbers aims to facilitate
  proofs
  involving basic arithmetical operations and order checking.
  It seems likely that the use of self-explanatory adjectives could also
  improve legibility of these proofs, which would be an important
  achievement \cite{pak2014improving}.
  Additionally, some potentially useful definitions, following those
  defined for real numbers, are introduced.
  }}

@article{pak2014improving,
  title={Improving legibility of natural deduction proofs is not trivial},
  author={P\k{a}k, Karol},
  journal={Logical Methods in Computer Science},
  volume={10},
  year={2014},
  publisher={Episciences.org}}
