# 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.

Lemma int_divides_lcm_in_seq:

∀ (x : nat) (xs : seq nat), x %| lcml (x :: xs).

Proof.

induction xs.

- by apply dvdn_lcml.

- rewrite /lcml -cat1s foldr_cat /foldr.

by apply dvdn_lcml.

Qed.

∀ (x : nat) (xs : seq nat), x %| lcml (x :: xs).

Proof.

induction xs.

- by apply dvdn_lcml.

- rewrite /lcml -cat1s foldr_cat /foldr.

by apply dvdn_lcml.

Qed.

Lemma lcm_seq_divides_lcm_super:

∀ (x : nat) (xs : seq nat),

lcml xs %| lcml (x :: xs).

Proof.

induction xs; first by auto.

rewrite /lcml -cat1s foldr_cat /foldr.

by apply dvdn_lcmr.

Qed.

∀ (x : nat) (xs : seq nat),

lcml xs %| lcml (x :: xs).

Proof.

induction xs; first by auto.

rewrite /lcml -cat1s foldr_cat /foldr.

by apply dvdn_lcmr.

Qed.

Lemma lcm_seq_is_mult_of_all_ints:

∀ (x : nat) (xs: seq nat), x \in xs → x %| lcml xs.

Proof.

intros x xs IN; apply/dvdnP.

induction xs as [ | z sq IH_DIV]; first by done.

rewrite in_cons in IN.

move : IN ⇒ /orP [/eqP EQ | IN].

- apply /dvdnP.

rewrite EQ /lcml.

by apply int_divides_lcm_in_seq.

+ move : (IH_DIV IN) ⇒ [k EQ].

∃ ((foldr lcmn 1 (z :: sq)) %/ (foldr lcmn 1 sq) × k).

rewrite -mulnA -EQ divnK /lcml //.

by apply lcm_seq_divides_lcm_super.

Qed.

∀ (x : nat) (xs: seq nat), x \in xs → x %| lcml xs.

Proof.

intros x xs IN; apply/dvdnP.

induction xs as [ | z sq IH_DIV]; first by done.

rewrite in_cons in IN.

move : IN ⇒ /orP [/eqP EQ | IN].

- apply /dvdnP.

rewrite EQ /lcml.

by apply int_divides_lcm_in_seq.

+ move : (IH_DIV IN) ⇒ [k EQ].

∃ ((foldr lcmn 1 (z :: sq)) %/ (foldr lcmn 1 sq) × k).

rewrite -mulnA -EQ divnK /lcml //.

by apply lcm_seq_divides_lcm_super.

Qed.

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.

Proof.

intros × POS.

induction xs; first by easy.

rewrite /lcml -cat1s //= lcmn_gt0.

apply/andP; split ⇒ //.

- by apply POS; rewrite in_cons eq_refl.

- apply: IHxs; intros b B_IN.

by apply POS; rewrite in_cons; apply /orP; right ⇒ //.

Qed.

∀ (xs : seq nat),

(∀ x, x \in xs → x > 0) →

lcml xs > 0.

Proof.

intros × POS.

induction xs; first by easy.

rewrite /lcml -cat1s //= lcmn_gt0.

apply/andP; split ⇒ //.

- by apply POS; rewrite in_cons eq_refl.

- apply: IHxs; intros b B_IN.

by apply POS; rewrite in_cons; apply /orP; right ⇒ //.

Qed.