Программирование вычислительной алгебры на основе конструктивной математики. Области с разложением на простые множители

Статья продолжает публикации автора о подходе к использованию конструктивной математики и применении языка с зависимыми типами для доказуемого программирования вычислительной алгебры.
Получено конструктивное выражение понятия области с разложением на простые множители для моноидa и кольца с некоторыми дополнительными свойствами. Описан способ построения машинно-проверяемых доказательств для теорем, связывающих понятия разложения на простые множители в областях различного вида.
Все описываемые построения и доказательства воплощены полностью в виде программы на функциональном языке Agda.