Найти наибольший общий делитель чисел m и n, перебирая числа от min m.

Написать программу на языке Сoq.

В Coq есть операция m mod n (или modulo m n), которая возвращает остаток от деления m на n. Однако поскольку все функции в Coq являются тотальными, значение выражения m mod 0 равно 0 по определению. Также есть предикат (n | m) (пишется в скобках; или divide n m), который равен True, если n делит m. Следует обратить внимание, что modulo возвращает nat и следовательно может быть использован в программах, в то время как divide n m возвращает Prop и может использоваться только в спецификациях.