Library com.io7m.entomos.Divisible

From Stdlib Require Import Arith.PeanoNat.
From Stdlib Require Import Lists.List.
From Stdlib Require Import Init.Nat.

Theorem divisiblityNAdd : ∀ (x y z : nat),
  0 ≠ z → x mod z = 0 → y mod z = 0 → (x + y) mod z = 0.
Proof.
  intros x y z Hz Hx Hy.
  destruct y as [|y].
    rewrite Nat.add_0_r; exact Hx.
    assert ((x mod z + S y) mod z = (x + S y) mod z) as Heq.
      apply (Nat.Div0.add_mod_idemp_l x (S y) z).
    rewrite Hx in Heq.
    rewrite Nat.add_0_l in Heq.
    rewrite <- Heq.
    exact Hy.
Qed.

Theorem divisibilityNFoldPlus : ∀ z xs,
  0 ≠ z →
    Forall (fun n ⇒ n mod z = 0) xs →
      (fold_right plus 0 xs) mod z = 0.
Proof.
  intros z xs Hnz HforAll.
  induction xs as [|y ys].
  - apply (Nat.Div0.mod_0_l z).
  - assert (fold_right add 0 (y :: ys) = y + fold_right add 0 ys) as Hfoldeq by reflexivity.
    rewrite Hfoldeq.
    assert (fold_right add 0 ys mod z = 0) as Hfoldeq2. {
      apply IHys.
      apply (@Forall_inv_tail nat (fun n : nat ⇒ n mod z = 0) y ys HforAll).
    }
    rewrite divisiblityNAdd.
    reflexivity.
    exact Hnz.
    apply (@Forall_inv nat (fun n : nat ⇒ n mod z = 0) y ys HforAll).
    exact Hfoldeq2.
Qed.