Library prosa.util.lcmseq

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

A function to calculate the least common multiple of all integers in a sequence xs, denoted by lcml xs
Definition lcml (xs : seq nat) : nat := foldr lcmn 1 xs.

Any integer a that is contained in the sequence xs divides lcml xs.
Lemma int_divides_lcm_in_seq:
   (a : nat) (xs : seq nat), a %| lcml (a :: xs).

Also, lcml xs1 divides lcml xs2 if xs2 contains one extra element as compared to xs1.
Lemma lcm_seq_divides_lcm_super:
   (x : nat) (xs : seq nat),
  lcml xs %| lcml (x :: xs).

All integers in a sequence xs divide lcml xs.
Lemma lcm_seq_is_mult_of_all_ints:
   (sq : seq nat) (a : nat), a \in sq k, lcml sq = k × a.

The LCM of all elements in a sequence with only positive elements is positive.
Lemma all_pos_implies_lcml_pos:
   (xs : seq nat),
    ( b, b \in xs b > 0)
    lcml xs > 0.