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.

First we show that x divides lcml (x :: xs) for any x and xs.
Lemma int_divides_lcm_in_seq:
  ∀ (x : nat) (xs : seq nat), x %| lcml (x :: xs).

Similarly, lcml xs divides lcml (x :: xs) for any x and xs.
Lemma lcm_seq_divides_lcm_super:
  ∀ (x : nat) (xs : seq nat),
  lcml xs %| lcml (x :: xs).

Given a sequence xs, any integer x \in xs divides lcml xs.
Lemma lcm_seq_is_mult_of_all_ints:
  ∀ (x : nat) (xs: seq nat), x \in xs → x %| lcml xs.

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