# Library prosa.util.lcmseq

From mathcomp Require Export ssreflect seq div ssrbool ssrnat eqtype ssrfun.

Require Export prosa.util.tactics.

Require Export prosa.util.tactics.

A function to calculate the least common multiple
of all integers in a sequence xs, denoted by lcml xs.

The LCM of all elements in a sequence with only positive elements is positive.