From Coq Require Import ZArith.Znumtheory.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
From stdpp Require Import prelude finite.[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From VLSM.Lib Require Import EquationsExtras.[Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
[Loading ML file equations_plugin.cmxs (using legacy method) ... done]
From VLSM.Lib Require Import Preamble FinSuppFn StdppExtras ListExtras.[Loading ML file coq-itauto.plugin ... done]

Utility: Natural Number Definitions and Results

Compute the list of all naturals less than n.

Fixpoint up_to_n_listing (n : nat) : list nat :=
  match n with
  | 0 => []
  | S n' => n' :: up_to_n_listing n'
  end.

Lemma up_to_n_listing_length :
  forall (n : nat),
    length (up_to_n_listing n) = n.∀ n : nat, length (up_to_n_listing n) = n
Proof.∀ n : nat, length (up_to_n_listing n) = n
  by induction n; simpl; congruence.
Qed.

Lemma up_to_n_full :
  forall (n i : nat),
    i < n <-> i ∈ up_to_n_listing n.∀ n i : nat, i < n ↔ i ∈ up_to_n_listing n
Proof.∀ n i : nat, i < n ↔ i ∈ up_to_n_listing n
  induction n; split; inversion 1; subst; cbn; [left | | lia |].n: nat
IHn: ∀ i : nat, i < n ↔ i ∈ up_to_n_listing n
i: nat
H: i < S n
H1: S i ≤ n
i ∈ n :: up_to_n_listing n
n: nat
IHn: ∀ i : nat, i < n ↔ i ∈ up_to_n_listing n
i: nat
H: i ∈ up_to_n_listing (S n)
H2: i ∈ up_to_n_listing n
i < S n
  -n: nat
IHn: ∀ i : nat, i < n ↔ i ∈ up_to_n_listing n
i: nat
H: i < S n
H1: S i ≤ n
i ∈ n :: up_to_n_listing n by right; apply IHn.
  -n: nat
IHn: ∀ i : nat, i < n ↔ i ∈ up_to_n_listing n
i: nat
H: i ∈ up_to_n_listing (S n)
H2: i ∈ up_to_n_listing n
i < S n by transitivity n; [apply IHn | lia].
Qed.

Given a decidable property on naturals and a bound, finds the largest natural (not larger the than bound) for which the property holds.

Equations find_largest_nat_with_property_bounded
  (P : nat -> Prop) `{forall n, Decision (P n)}
  (bound : nat)
  : option nat :=
| P, 0 => None
| P, S n => if decide (P n) then Some n else find_largest_nat_with_property_bounded P n.

Lemma find_largest_nat_with_property_bounded_Some
  (P : nat -> Prop) `{forall n, Decision (P n)}
  (bound : nat)
  : forall n,
      find_largest_nat_with_property_bounded P bound = Some n
        <->
      maximal_among lt (fun n => n < bound /\ P n) n.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
∀ n : nat,
  find_largest_nat_with_property_bounded P bound =
  Some n
  ↔ maximal_among lt (λ n0 : nat, n0 < bound ∧ P n0) n
Proof.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
∀ n : nat,
  find_largest_nat_with_property_bounded P bound =
  Some n
  ↔ maximal_among lt (λ n0 : nat, n0 < bound ∧ P n0) n
  induction bound; simp find_largest_nat_with_property_bounded.P: nat → Prop
H: ∀ n : nat, Decision (P n)
∀ n : nat,
  None = Some n
  ↔ maximal_among lt (λ n0 : nat, n0 < 0 ∧ P n0) n
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
∀ n : nat,
  (if decide (P bound)
   then Some bound
   else find_largest_nat_with_property_bounded P bound) =
  Some n
  ↔ maximal_among lt (λ n0 : nat, n0 < S bound ∧ P n0)
      n
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
∀ n : nat,
  None = Some n
  ↔ maximal_among lt (λ n0 : nat, n0 < 0 ∧ P n0) n by split; [| intros []; lia].
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
∀ n : nat,
  (if decide (P bound)
   then Some bound
   else find_largest_nat_with_property_bounded P bound) =
  Some n
  ↔ maximal_among lt (λ n0 : nat, n0 < S bound ∧ P n0)
      n case_decide as HP; split.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: P bound
n: nat
Some bound = Some n
→ maximal_among lt (λ n : nat, n < S bound ∧ P n) n
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: P bound
n: nat
maximal_among lt (λ n : nat, n < S bound ∧ P n) n
→ Some bound = Some n
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
find_largest_nat_with_property_bounded P bound =
Some n
→ maximal_among lt (λ n : nat, n < S bound ∧ P n) n
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
maximal_among lt (λ n : nat, n < S bound ∧ P n) n
→ find_largest_nat_with_property_bounded P bound =
  Some n
    +P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: P bound
n: nat
Some bound = Some n
→ maximal_among lt (λ n : nat, n < S bound ∧ P n) n by intros [= ->]; repeat split; cbn; [lia | | lia].
    +P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: P bound
n: nat
maximal_among lt (λ n : nat, n < S bound ∧ P n) n
→ Some bound = Some n intros [[Hn HPn] Hmax]; f_equal; cbn in Hmax.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: P bound
n: nat
Hn: n < S bound
HPn: P n
Hmax: ∀ m' : nat,
  m' < S bound ∧ P m' → n < m' → m' < n
bound = n
      destruct (decide (n < bound)); [| lia].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: P bound
n: nat
Hn: n < S bound
HPn: P n
Hmax: ∀ m' : nat,
  m' < S bound ∧ P m' → n < m' → m' < n
l: n < bound
bound = n
      cut (bound < n); [lia |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: P bound
n: nat
Hn: n < S bound
HPn: P n
Hmax: ∀ m' : nat,
  m' < S bound ∧ P m' → n < m' → m' < n
l: n < bound
bound < n
      by apply Hmax; [split; [lia |] |].
    +P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
find_largest_nat_with_property_bounded P bound =
Some n
→ maximal_among lt (λ n : nat, n < S bound ∧ P n) n rewrite IHbound.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
maximal_among lt (λ n : nat, n < bound ∧ P n) n
→ maximal_among lt (λ n : nat, n < S bound ∧ P n) n
      intros [[] Hmax]; split; [by split; [lia |] |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
H0: n < bound
H1: P n
Hmax: ∀ m' : nat,
  m' < bound ∧ P m'
  → flip lt m' n → flip lt n m'
∀ m' : nat,
  m' < S bound ∧ P m' → flip lt m' n → flip lt n m'
      intros m [] ?.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
H0: n < bound
H1: P n
Hmax: ∀ m' : nat,
  m' < bound ∧ P m'
  → flip lt m' n → flip lt n m'
m: nat
H2: m < S bound
H3: P m
H4: flip lt m n
flip lt n m
      apply Hmax; [split; [| done] | done].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
H0: n < bound
H1: P n
Hmax: ∀ m' : nat,
  m' < bound ∧ P m'
  → flip lt m' n → flip lt n m'
m: nat
H2: m < S bound
H3: P m
H4: flip lt m n
m < bound
      by destruct (decide (m = bound)); [subst | lia].
    +P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
maximal_among lt (λ n : nat, n < S bound ∧ P n) n
→ find_largest_nat_with_property_bounded P bound =
  Some n intros [[] Hmax]; apply IHbound; repeat split; [| done |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
H0: n < S bound
H1: P n
Hmax: ∀ m' : nat,
  m' < S bound ∧ P m'
  → flip lt m' n → flip lt n m'
n < bound
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
H0: n < S bound
H1: P n
Hmax: ∀ m' : nat,
  m' < S bound ∧ P m'
  → flip lt m' n → flip lt n m'
∀ m' : nat,
  m' < bound ∧ P m' → flip lt m' n → flip lt n m'
      *P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
H0: n < S bound
H1: P n
Hmax: ∀ m' : nat,
  m' < S bound ∧ P m'
  → flip lt m' n → flip lt n m'
n < bound by destruct (decide (n = bound)); [subst | lia].
      *P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: ∀ n : nat,
  find_largest_nat_with_property_bounded P
    bound = Some n
  ↔ maximal_among lt
      (λ n0 : nat, n0 < bound ∧ P n0) n
HP: ¬ P bound
n: nat
H0: n < S bound
H1: P n
Hmax: ∀ m' : nat,
  m' < S bound ∧ P m'
  → flip lt m' n → flip lt n m'
∀ m' : nat,
  m' < bound ∧ P m' → flip lt m' n → flip lt n m' by intros m [] ?; apply Hmax; [split; [lia |] |].
Qed.

Lemma find_largest_nat_with_property_bounded_None
  (P : nat -> Prop) `{forall n, Decision (P n)}
  (bound : nat)
  : find_largest_nat_with_property_bounded P bound = None
      <->
    forall n, n < bound -> ~ P n.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
find_largest_nat_with_property_bounded P bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
Proof.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
find_largest_nat_with_property_bounded P bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
  induction bound; simp find_largest_nat_with_property_bounded; [by split; [lia |] |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
(if decide (P bound)
 then Some bound
 else find_largest_nat_with_property_bounded P bound) =
None ↔ (∀ n : nat, n < S bound → ¬ P n)
  case_decide as HP; split; [done | | |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: P bound
(∀ n : nat, n < S bound → ¬ P n) → Some bound = None
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: ¬ P bound
find_largest_nat_with_property_bounded P bound = None
→ ∀ n : nat, n < S bound → ¬ P n
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: ¬ P bound
(∀ n : nat, n < S bound → ¬ P n)
→ find_largest_nat_with_property_bounded P bound =
  None
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: P bound
(∀ n : nat, n < S bound → ¬ P n) → Some bound = None by intro Hmax; contradict HP; apply Hmax; lia.
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: ¬ P bound
find_largest_nat_with_property_bounded P bound = None
→ ∀ n : nat, n < S bound → ¬ P n intros.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: ¬ P bound
H0: find_largest_nat_with_property_bounded P bound =
None
n: nat
H1: n < S bound
¬ P n
    destruct (decide (n < bound)); [by eapply IHbound |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: ¬ P bound
H0: find_largest_nat_with_property_bounded P bound =
None
n: nat
H1: n < S bound
n0: ¬ n < bound
¬ P n
    by replace n with bound; [| lia].
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: ¬ P bound
(∀ n : nat, n < S bound → ¬ P n)
→ find_largest_nat_with_property_bounded P bound =
  None intros Hmax; apply IHbound.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
IHbound: find_largest_nat_with_property_bounded P
  bound = None
↔ (∀ n : nat, n < bound → ¬ P n)
HP: ¬ P bound
Hmax: ∀ n : nat, n < S bound → ¬ P n
∀ n : nat, n < bound → ¬ P n
    by intros; apply Hmax; lia.
Qed.

Given a predicate on indices and naturals, a bound for each index, and a list of indices, finds first index in the list and largest natural (less than bound) corresponding to it for which the predicate holds.

Equations find_first_indexed_largest_nat_with_propery_bounded {index}
  (P : index -> nat -> Prop) `{!RelDecision P}
  (bound : index -> nat)
  (indices : list index)
  : option (index * nat) :=
| _, _, [] => None
| P, bound, i :: indices' with inspect (find_largest_nat_with_property_bounded (P i) (bound i)) =>
  | None eq: Hdec => find_first_indexed_largest_nat_with_propery_bounded P bound indices';
  | (Some n) eq: Hdec => Some (i, n).

Lemma find_first_indexed_largest_nat_with_propery_bounded_Some {index}
  (P : index -> nat -> Prop) `{!RelDecision P}
  (bound : index -> nat)
  (indices : list index) (Hindices : NoDup indices)
  : forall (i : index) (n : nat),
      find_first_indexed_largest_nat_with_propery_bounded P bound indices = Some (i, n)
        <->
      i ∈ indices /\
      find_largest_nat_with_property_bounded (P i) (bound i) = Some n /\
      forall (prefix suffix : list index),
        indices = prefix ++ [i] ++ suffix ->
        forall (j : index), j ∈ prefix ->
        find_largest_nat_with_property_bounded (P j) (bound j) = None.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
indices: list index
Hindices: NoDup indices
∀ (i : index) (n : nat),
  find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = Some (i, n)
  ↔ i ∈ indices
    ∧ find_largest_nat_with_property_bounded (P i)
        (bound i) = Some n
      ∧ (∀ prefix suffix : list index,
           indices = prefix ++ [i] ++ suffix
           → ∀ j : index,
               j ∈ prefix
               → find_largest_nat_with_property_bounded
                   (P j) (bound j) = None)
Proof.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
indices: list index
Hindices: NoDup indices
∀ (i : index) (n : nat),
  find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = Some (i, n)
  ↔ i ∈ indices
    ∧ find_largest_nat_with_property_bounded (P i)
        (bound i) = Some n
      ∧ (∀ prefix suffix : list index,
           indices = prefix ++ [i] ++ suffix
           → ∀ j : index,
               j ∈ prefix
               → find_largest_nat_with_property_bounded
                   (P j) (bound j) = None)
  induction indices; simp find_first_indexed_largest_nat_with_propery_bounded.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
Hindices: NoDup []
∀ (i : index) (n : nat),
  None = Some (i, n)
  ↔ i ∈ []
    ∧ find_largest_nat_with_property_bounded (P i)
        (bound i) = Some n
      ∧ (∀ prefix suffix : list index,
           [] = prefix ++ [i] ++ suffix
           → ∀ j : index,
               j ∈ prefix
               → find_largest_nat_with_property_bounded
                   (P j) (bound j) = None)
index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Hindices: NoDup (a :: indices)
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
∀ (i : index) (n : nat),
  find_first_indexed_largest_nat_with_propery_bounded_clause_2
    (@find_first_indexed_largest_nat_with_propery_bounded)
    index P RelDecision0 bound a
    (inspect
       (find_largest_nat_with_property_bounded 
          (P a) (bound a))) indices = 
  Some (i, n)
  ↔ i ∈ a :: indices
    ∧ find_largest_nat_with_property_bounded 
        (P i) (bound i) = 
      Some n
      ∧ (∀ prefix suffix : list index,
           a :: indices = prefix ++ [i] ++ suffix
           → ∀ j : index,
               j ∈ prefix
               → find_largest_nat_with_property_bounded
                   (P j) 
                   (bound j) = None)
  -index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
Hindices: NoDup []
∀ (i : index) (n : nat),
  None = Some (i, n)
  ↔ i ∈ []
    ∧ find_largest_nat_with_property_bounded (P i)
        (bound i) = Some n
      ∧ (∀ prefix suffix : list index,
           [] = prefix ++ [i] ++ suffix
           → ∀ j : index,
               j ∈ prefix
               → find_largest_nat_with_property_bounded
                   (P j) (bound j) = None) by split; [inversion 1 | intros [Hcontra]; inversion Hcontra].
  -index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Hindices: NoDup (a :: indices)
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
∀ (i : index) (n : nat),
  find_first_indexed_largest_nat_with_propery_bounded_clause_2
    (@find_first_indexed_largest_nat_with_propery_bounded)
    index P RelDecision0 bound a
    (inspect
       (find_largest_nat_with_property_bounded (P a)
          (bound a))) indices = Some (i, n)
  ↔ i ∈ a :: indices
    ∧ find_largest_nat_with_property_bounded (P i)
        (bound i) = Some n
      ∧ (∀ prefix suffix : list index,
           a :: indices = prefix ++ [i] ++ suffix
           → ∀ j : index,
               j ∈ prefix
               → find_largest_nat_with_property_bounded
                   (P j) (bound j) = None) apply NoDup_cons in Hindices as [Ha Hindices].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
∀ (i : index) (n : nat),
  find_first_indexed_largest_nat_with_propery_bounded_clause_2
    (@find_first_indexed_largest_nat_with_propery_bounded)
    index P RelDecision0 bound a
    (inspect
       (find_largest_nat_with_property_bounded (P a)
          (bound a))) indices = Some (i, n)
  ↔ i ∈ a :: indices
    ∧ find_largest_nat_with_property_bounded (P i)
        (bound i) = Some n
      ∧ (∀ prefix suffix : list index,
           a :: indices = prefix ++ [i] ++ suffix
           → ∀ j : index,
               j ∈ prefix
               → find_largest_nat_with_property_bounded
                   (P j) (bound j) = None)
    cbn; split;
      destruct (find_largest_nat_with_property_bounded  (P a) (bound a)) as [_n |] eqn: Hpos.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n, _n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some _n
Some (a, _n) = Some (i, n)
→ i ∈ a :: indices
  ∧ find_largest_nat_with_property_bounded (P i)
      (bound i) = Some n
    ∧ (∀ prefix suffix : list index,
         a :: indices = prefix ++ i :: suffix
         → ∀ j : index,
             j ∈ prefix
             → find_largest_nat_with_property_bounded
                 (P j) (bound j) = None)
index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = Some (i, n)
→ i ∈ a :: indices
  ∧ find_largest_nat_with_property_bounded 
      (P i) (bound i) = 
    Some n
    ∧ (∀ prefix suffix : list index,
         a :: indices = prefix ++ i :: suffix
         → ∀ j : index,
             j ∈ prefix
             → find_largest_nat_with_property_bounded
                 (P j) (bound j) = None)
index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n, _n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some _n
i ∈ a :: indices
∧ find_largest_nat_with_property_bounded 
    (P i) (bound i) = Some n
  ∧ (∀ prefix suffix : list index,
       a :: indices = prefix ++ i :: suffix
       → ∀ j : index,
           j ∈ prefix
           → find_largest_nat_with_property_bounded
               (P j) (bound j) = None)
→ Some (a, _n) = Some (i, n)
index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
i ∈ a :: indices
∧ find_largest_nat_with_property_bounded 
    (P i) (bound i) = Some n
  ∧ (∀ prefix suffix : list index,
       a :: indices = prefix ++ i :: suffix
       → ∀ j : index,
           j ∈ prefix
           → find_largest_nat_with_property_bounded
               (P j) (bound j) = None)
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = Some (i, n)
    +index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n, _n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some _n
Some (a, _n) = Some (i, n)
→ i ∈ a :: indices
  ∧ find_largest_nat_with_property_bounded (P i)
      (bound i) = Some n
    ∧ (∀ prefix suffix : list index,
         a :: indices = prefix ++ i :: suffix
         → ∀ j : index,
             j ∈ prefix
             → find_largest_nat_with_property_bounded
                 (P j) (bound j) = None) inversion 1; subst a _n; split_and!; [by left | done |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
indices: list index
i: index
Ha: i ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
H: Some (i, n) = Some (i, n)
∀ prefix suffix : list index,
  i :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded (P j)
          (bound j) = None
      intros [| _i prefix] ? Heq; [by inversion 1 |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
indices: list index
i: index
Ha: i ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
H: Some (i, n) = Some (i, n)
_i: index
prefix, suffix: list index
Heq: i :: indices = (_i :: prefix) ++ i :: suffix
∀ j : index,
  j ∈ _i :: prefix
  → find_largest_nat_with_property_bounded (P j)
      (bound j) = None
      contradict Ha; simplify_list_eq.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
prefix, suffix: list index
_i: index
Hindices: NoDup (prefix ++ _i :: suffix)
IHindices: NoDup (prefix ++ _i :: suffix)
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound (prefix ++ _i :: suffix) =
    Some (i, n)
    ↔ i ∈ prefix ++ _i :: suffix
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix0 suffix0 : list index,
             prefix ++ _i :: suffix =
             prefix0 ++ i :: suffix0
             → ∀ j : index,
                 j ∈ prefix0
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P _i) (bound _i) = Some n
_i ∈ prefix ++ _i :: suffix
      by apply elem_of_app; right; left.
    +index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = Some (i, n)
→ i ∈ a :: indices
  ∧ find_largest_nat_with_property_bounded (P i)
      (bound i) = Some n
    ∧ (∀ prefix suffix : list index,
         a :: indices = prefix ++ i :: suffix
         → ∀ j : index,
             j ∈ prefix
             → find_largest_nat_with_property_bounded
                 (P j) (bound j) = None) rewrite IHindices by done.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
i ∈ indices
∧ find_largest_nat_with_property_bounded (P i)
    (bound i) = Some n
  ∧ (∀ prefix suffix : list index,
       indices = prefix ++ [i] ++ suffix
       → ∀ j : index,
           j ∈ prefix
           → find_largest_nat_with_property_bounded
               (P j) (bound j) = None)
→ i ∈ a :: indices
  ∧ find_largest_nat_with_property_bounded (P i)
      (bound i) = Some n
    ∧ (∀ prefix suffix : list index,
         a :: indices = prefix ++ i :: suffix
         → ∀ j : index,
             j ∈ prefix
             → find_largest_nat_with_property_bounded
                 (P j) (bound j) = None)
      intros (Hi & Hposition & Hfirst).index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ indices
Hposition: find_largest_nat_with_property_bounded
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  indices = prefix ++ [i] ++ suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
i ∈ a :: indices
∧ find_largest_nat_with_property_bounded (P i)
    (bound i) = Some n
  ∧ (∀ prefix suffix : list index,
       a :: indices = prefix ++ i :: suffix
       → ∀ j : index,
           j ∈ prefix
           → find_largest_nat_with_property_bounded
               (P j) (bound j) = None)
      split_and!; [by right | done |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ indices
Hposition: find_largest_nat_with_property_bounded
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  indices = prefix ++ [i] ++ suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
∀ prefix suffix : list index,
  a :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded (P j)
          (bound j) = None
      intros [| _a prefix] ? Heq; [by inversion 1 |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ indices
Hposition: find_largest_nat_with_property_bounded
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  indices = prefix ++ [i] ++ suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
_a: index
prefix, suffix: list index
Heq: a :: indices = (_a :: prefix) ++ i :: suffix
∀ j : index,
  j ∈ _a :: prefix
  → find_largest_nat_with_property_bounded (P j)
      (bound j) = None
      simplify_list_eq.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
i: index
prefix, suffix: list index
IHindices: NoDup (prefix ++ i :: suffix)
→ ∀ (i0 : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound (prefix ++ i :: suffix) =
    Some (i0, n)
    ↔ i0 ∈ prefix ++ i :: suffix
      ∧ find_largest_nat_with_property_bounded
          (P i0) (bound i0) = 
        Some n
        ∧ (∀ prefix0 suffix0 : list index,
             prefix ++ i :: suffix =
             prefix0 ++ i0 :: suffix0
             → ∀ j : index,
                 j ∈ prefix0
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
Hindices: NoDup (prefix ++ i :: suffix)
_a: index
Ha: _a ∉ prefix ++ i :: suffix
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P _a) (bound _a) = None
Hi: i ∈ prefix ++ i :: suffix
Hposition: find_largest_nat_with_property_bounded
  (P i) (bound i) = Some n
Hfirst: ∀ prefix0 suffix0 : list index,
  prefix ++ i :: suffix =
  prefix0 ++ i :: suffix0
  → ∀ j : index,
      j ∈ prefix0
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
∀ j : index,
  j ∈ _a :: prefix
  → find_largest_nat_with_property_bounded (P j)
      (bound j) = None
      by inversion 1; [| eapply Hfirst].
    +index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n, _n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some _n
i ∈ a :: indices
∧ find_largest_nat_with_property_bounded (P i)
    (bound i) = Some n
  ∧ (∀ prefix suffix : list index,
       a :: indices = prefix ++ i :: suffix
       → ∀ j : index,
           j ∈ prefix
           → find_largest_nat_with_property_bounded
               (P j) (bound j) = None)
→ Some (a, _n) = Some (i, n) intros (Hi & Hposi & Hfirst).index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n, _n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some _n
Hi: i ∈ a :: indices
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  a :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
Some (a, _n) = Some (i, n)
      apply elem_of_cons in Hi as [<- | Hi]; [by congruence |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n, _n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some _n
Hi: i ∈ indices
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  a :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
Some (a, _n) = Some (i, n)
      apply elem_of_list_split in Hi as (prefix' & suffix & ->).index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a, i: index
prefix', suffix: list index
IHindices: NoDup (prefix' ++ i :: suffix)
→ ∀ (i0 : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound (prefix' ++ i :: suffix) =
    Some (i0, n)
    ↔ i0 ∈ prefix' ++ i :: suffix
      ∧ find_largest_nat_with_property_bounded
          (P i0) (bound i0) = 
        Some n
        ∧ (∀ prefix suffix0 : list index,
             prefix' ++ i :: suffix =
             prefix ++ [i0] ++ suffix0
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
Hindices: NoDup (prefix' ++ i :: suffix)
Ha: a ∉ prefix' ++ i :: suffix
n, _n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some _n
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix0 : list index,
  a :: prefix' ++ i :: suffix =
  prefix ++ i :: suffix0
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
Some (a, _n) = Some (i, n)
      by erewrite Hfirst in Hpos; [| rewrite app_comm_cons | left].
    +index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
i ∈ a :: indices
∧ find_largest_nat_with_property_bounded (P i)
    (bound i) = Some n
  ∧ (∀ prefix suffix : list index,
       a :: indices = prefix ++ i :: suffix
       → ∀ j : index,
           j ∈ prefix
           → find_largest_nat_with_property_bounded
               (P j) (bound j) = None)
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = Some (i, n) intros (Hi & Hposi & Hfirst).index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ a :: indices
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  a :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = Some (i, n)
      apply elem_of_cons in Hi as [<- | Hi]; [by congruence |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ indices
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  a :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = Some (i, n)
      apply IHindices; [done |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ indices
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  a :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
i ∈ indices
∧ find_largest_nat_with_property_bounded (P i)
    (bound i) = Some n
  ∧ (∀ prefix suffix : list index,
       indices = prefix ++ [i] ++ suffix
       → ∀ j : index,
           j ∈ prefix
           → find_largest_nat_with_property_bounded
               (P j) (bound j) = None)
      split_and!; [done.. |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ ∀ (i : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound indices = 
    Some (i, n)
    ↔ i ∈ indices
      ∧ find_largest_nat_with_property_bounded
          (P i) (bound i) = 
        Some n
        ∧ (∀ prefix suffix : list index,
             indices =
             prefix ++ [i] ++ suffix
             → ∀ j : index,
                 j ∈ prefix
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
i: index
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ indices
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix suffix : list index,
  a :: indices = prefix ++ i :: suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
∀ prefix suffix : list index,
  indices = prefix ++ [i] ++ suffix
  → ∀ j : index,
      j ∈ prefix
      → find_largest_nat_with_property_bounded (P j)
          (bound j) = None
      intros prefix suffix -> j Hj.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a, i: index
prefix, suffix: list index
IHindices: NoDup (prefix ++ [i] ++ suffix)
→ ∀ (i0 : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound (prefix ++ [i] ++ suffix) =
    Some (i0, n)
    ↔ i0 ∈ prefix ++ [i] ++ suffix
      ∧ find_largest_nat_with_property_bounded
          (P i0) (bound i0) = 
        Some n
        ∧ (∀ prefix0 suffix0 : list index,
             prefix ++ [i] ++ suffix =
             prefix0 ++ [i0] ++ suffix0
             → ∀ j : index,
                 j ∈ prefix0
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
Hindices: NoDup (prefix ++ [i] ++ suffix)
Ha: a ∉ prefix ++ [i] ++ suffix
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ prefix ++ [i] ++ suffix
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix0 suffix0 : list index,
  a :: prefix ++ [i] ++ suffix =
  prefix0 ++ i :: suffix0
  → ∀ j : index,
      j ∈ prefix0
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
j: index
Hj: j ∈ prefix
find_largest_nat_with_property_bounded (P j) (bound j) =
None
      eapply Hfirst; [| by right].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a, i: index
prefix, suffix: list index
IHindices: NoDup (prefix ++ [i] ++ suffix)
→ ∀ (i0 : index) (n : nat),
    find_first_indexed_largest_nat_with_propery_bounded
      P bound (prefix ++ [i] ++ suffix) =
    Some (i0, n)
    ↔ i0 ∈ prefix ++ [i] ++ suffix
      ∧ find_largest_nat_with_property_bounded
          (P i0) (bound i0) = 
        Some n
        ∧ (∀ prefix0 suffix0 : list index,
             prefix ++ [i] ++ suffix =
             prefix0 ++ [i0] ++ suffix0
             → ∀ j : index,
                 j ∈ prefix0
                 → find_largest_nat_with_property_bounded
                     (P j) 
                     (bound j) = None)
Hindices: NoDup (prefix ++ [i] ++ suffix)
Ha: a ∉ prefix ++ [i] ++ suffix
n: nat
Hpos: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hi: i ∈ prefix ++ [i] ++ suffix
Hposi: find_largest_nat_with_property_bounded 
  (P i) (bound i) = Some n
Hfirst: ∀ prefix0 suffix0 : list index,
  a :: prefix ++ [i] ++ suffix =
  prefix0 ++ i :: suffix0
  → ∀ j : index,
      j ∈ prefix0
      → find_largest_nat_with_property_bounded
          (P j) (bound j) = None
j: index
Hj: j ∈ prefix
a :: prefix ++ [i] ++ suffix =
(?y :: prefix) ++ i :: ?suffix
      by rewrite app_comm_cons.
Qed.

Lemma find_first_indexed_largest_nat_with_propery_bounded_None {index}
  (P : index -> nat -> Prop) `{!RelDecision P}
  (bound : index -> nat)
  (indices : list index) (Hindices : NoDup indices)
  : find_first_indexed_largest_nat_with_propery_bounded P bound indices = None
      <->
    forall (i : index), i ∈ indices ->
      find_largest_nat_with_property_bounded (P i) (bound i) = None.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
indices: list index
Hindices: NoDup indices
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = None
↔ (∀ i : index,
     i ∈ indices
     → find_largest_nat_with_property_bounded (P i)
         (bound i) = None)
Proof.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
indices: list index
Hindices: NoDup indices
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = None
↔ (∀ i : index,
     i ∈ indices
     → find_largest_nat_with_property_bounded (P i)
         (bound i) = None)
  induction indices; simp find_first_indexed_largest_nat_with_propery_bounded;
    [by split; [inversion 2 |] |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Hindices: NoDup (a :: indices)
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
find_first_indexed_largest_nat_with_propery_bounded_clause_2
  (@find_first_indexed_largest_nat_with_propery_bounded)
  index P RelDecision0 bound a
  (inspect
     (find_largest_nat_with_property_bounded (P a)
        (bound a))) indices = None
↔ (∀ i : index,
     i ∈ a :: indices
     → find_largest_nat_with_property_bounded (P i)
         (bound i) = None)
  apply NoDup_cons in Hindices as [Ha Hindices].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
find_first_indexed_largest_nat_with_propery_bounded_clause_2
  (@find_first_indexed_largest_nat_with_propery_bounded)
  index P RelDecision0 bound a
  (inspect
     (find_largest_nat_with_property_bounded (P a)
        (bound a))) indices = None
↔ (∀ i : index,
     i ∈ a :: indices
     → find_largest_nat_with_property_bounded (P i)
         (bound i) = None)
  cbn; split; destruct find_largest_nat_with_property_bounded eqn: Hp; [done | | |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = None
→ ∀ i : index,
    i ∈ a :: indices
    → find_largest_nat_with_property_bounded (P i)
        (bound i) = None
index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
n: nat
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some n
(∀ i : index,
   i ∈ a :: indices
   → find_largest_nat_with_property_bounded 
       (P i) (bound i) = None) → 
Some (a, n) = None
index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
(∀ i : index,
   i ∈ a :: indices
   → find_largest_nat_with_property_bounded 
       (P i) (bound i) = None)
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  -index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = None
→ ∀ i : index,
    i ∈ a :: indices
    → find_largest_nat_with_property_bounded (P i)
        (bound i) = None by intros Hnone i Hi; apply elem_of_cons in Hi as  [-> | Hi]; [| eapply IHindices].
  -index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
n: nat
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some n
(∀ i : index,
   i ∈ a :: indices
   → find_largest_nat_with_property_bounded (P i)
       (bound i) = None) → Some (a, n) = None intro Hmin.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
n: nat
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some n
Hmin: ∀ i : index,
  i ∈ a :: indices
  → find_largest_nat_with_property_bounded
      (P i) (bound i) = None
Some (a, n) = None
    replace (find_largest_nat_with_property_bounded (P a) (bound a))
      with (@None nat) in Hp; [done |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
n: nat
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = Some n
Hmin: ∀ i : index,
  i ∈ a :: indices
  → find_largest_nat_with_property_bounded
      (P i) (bound i) = None
None =
find_largest_nat_with_property_bounded (P a) (bound a)
    by symmetry; apply Hmin; left.
  -index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
(∀ i : index,
   i ∈ a :: indices
   → find_largest_nat_with_property_bounded (P i)
       (bound i) = None)
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None intros Hmin.index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hmin: ∀ i : index,
  i ∈ a :: indices
  → find_largest_nat_with_property_bounded
      (P i) (bound i) = None
find_first_indexed_largest_nat_with_propery_bounded P
  bound indices = None
    apply IHindices; [done |].index: Type
P: index → nat → Prop
RelDecision0: RelDecision P
bound: index → nat
a: index
indices: list index
Ha: a ∉ indices
Hindices: NoDup indices
IHindices: NoDup indices
→ find_first_indexed_largest_nat_with_propery_bounded
    P bound indices = None
  ↔ (∀ i : index,
       i ∈ indices
       → find_largest_nat_with_property_bounded
           (P i) (bound i) = None)
Hp: find_largest_nat_with_property_bounded 
  (P a) (bound a) = None
Hmin: ∀ i : index,
  i ∈ a :: indices
  → find_largest_nat_with_property_bounded
      (P i) (bound i) = None
∀ i : index,
  i ∈ indices
  → find_largest_nat_with_property_bounded (P i)
      (bound i) = None
    by intros; apply Hmin; right.
Qed.

Products of (natural) powers of integers

Section sec_prod_powers.

Context
  `{EqDecision index}
  `(multipliers : index -> Z)
  .

Despite being functions, multipliers are supposed to represent a list [m_1, ..., m_n] and powers are supposed to represent a list [p_1, ..., p_n]. The function computes m_1^p_1 * ... * m_n^p_n.

Definition prod_powers_aux (powers : index -> nat) (l : list index) : Z :=
  foldr Z.mul 1%Z (zip_with Z.pow (map multipliers l) (map (Z.of_nat ∘ powers) l)).

#[export] Instance prod_powers_aux_proper :
  Proper ((=) ==> (≡ₚ) ==> (=)) prod_powers_aux.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (eq ==> Permutation ==> eq) prod_powers_aux
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (eq ==> Permutation ==> eq) prod_powers_aux
  intros _f f ->.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: index → nat
(Permutation ==> eq)%signature (prod_powers_aux f)
  (prod_powers_aux f)
  induction 1; cbn; [done | ..].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: index → nat
x: index
l, l': list index
H: l ≡ₚ l'
IHPermutation: prod_powers_aux f l =
prod_powers_aux f l'
(multipliers x ^ Z.of_nat (f x) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ f) l)))%Z =
(multipliers x ^ Z.of_nat (f x) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l')
      (map (Z.of_nat ∘ f) l')))%Z
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: index → nat
x, y: index
l: list index
(multipliers y ^ Z.of_nat (f y) *
 (multipliers x ^ Z.of_nat (f x) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z =
(multipliers x ^ Z.of_nat (f x) *
 (multipliers y ^ Z.of_nat (f y) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: index → nat
l, l', l'': list index
H: l ≡ₚ l'
H0: l' ≡ₚ l''
IHPermutation1: prod_powers_aux f l =
prod_powers_aux f l'
IHPermutation2: prod_powers_aux f l' =
prod_powers_aux f l''
prod_powers_aux f l = prod_powers_aux f l''
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: index → nat
x: index
l, l': list index
H: l ≡ₚ l'
IHPermutation: prod_powers_aux f l =
prod_powers_aux f l'
(multipliers x ^ Z.of_nat (f x) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ f) l)))%Z =
(multipliers x ^ Z.of_nat (f x) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l')
      (map (Z.of_nat ∘ f) l')))%Z by setoid_rewrite IHPermutation.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: index → nat
x, y: index
l: list index
(multipliers y ^ Z.of_nat (f y) *
 (multipliers x ^ Z.of_nat (f x) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z =
(multipliers x ^ Z.of_nat (f x) *
 (multipliers y ^ Z.of_nat (f y) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z by lia.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: index → nat
l, l', l'': list index
H: l ≡ₚ l'
H0: l' ≡ₚ l''
IHPermutation1: prod_powers_aux f l =
prod_powers_aux f l'
IHPermutation2: prod_powers_aux f l' =
prod_powers_aux f l''
prod_powers_aux f l = prod_powers_aux f l'' by congruence.
Qed.

Lemma prod_powers_aux_ext_forall (powers1 powers2 : index -> nat) (l : list index) :
  (forall i, i ∈ l -> powers1 i = powers2 i) ->
  prod_powers_aux powers1 l = prod_powers_aux powers2 l.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers1, powers2: index → nat
l: list index
(∀ i : index, i ∈ l → powers1 i = powers2 i)
→ prod_powers_aux powers1 l =
  prod_powers_aux powers2 l
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers1, powers2: index → nat
l: list index
(∀ i : index, i ∈ l → powers1 i = powers2 i)
→ prod_powers_aux powers1 l =
  prod_powers_aux powers2 l
  intros Hall; unfold prod_powers_aux.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers1, powers2: index → nat
l: list index
Hall: ∀ i : index, i ∈ l → powers1 i = powers2 i
foldr Z.mul 1%Z
  (zip_with Z.pow (map multipliers l)
     (map (Z.of_nat ∘ powers1) l)) =
foldr Z.mul 1%Z
  (zip_with Z.pow (map multipliers l)
     (map (Z.of_nat ∘ powers2) l))
  do 2 f_equal.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers1, powers2: index → nat
l: list index
Hall: ∀ i : index, i ∈ l → powers1 i = powers2 i
map (Z.of_nat ∘ powers1) l =
map (Z.of_nat ∘ powers2) l
  apply map_ext_Forall, Forall_forall.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers1, powers2: index → nat
l: list index
Hall: ∀ i : index, i ∈ l → powers1 i = powers2 i
∀ x : index,
  x ∈ l
  → (Z.of_nat ∘ powers1) x = (Z.of_nat ∘ powers2) x
  by intros; cbn; f_equal; apply Hall.
Qed.

Lemma prod_powers_aux_ge_1 (powers : index -> nat) (l : list index)
  (Hmpos : Forall (fun i => (multipliers i > 0)%Z) l) :
  (prod_powers_aux powers l >= 1)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
l: list index
Hmpos: Forall (λ i : index, (multipliers i > 0)%Z) l
(prod_powers_aux powers l >= 1)%Z
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
l: list index
Hmpos: Forall (λ i : index, (multipliers i > 0)%Z) l
(prod_powers_aux powers l >= 1)%Z
  revert Hmpos; induction l; [by cbn; lia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
IHl: Forall (λ i : index, (multipliers i > 0)%Z) l
→ (prod_powers_aux powers l >= 1)%Z
Forall (λ i : index, (multipliers i > 0)%Z) (a :: l)
→ (prod_powers_aux powers (a :: l) >= 1)%Z
  rewrite Forall_cons; intros [Hma Hmpos].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
IHl: Forall (λ i : index, (multipliers i > 0)%Z) l
→ (prod_powers_aux powers l >= 1)%Z
Hma: (multipliers a > 0)%Z
Hmpos: Forall (λ i : index, (multipliers i > 0)%Z) l
(prod_powers_aux powers (a :: l) >= 1)%Z
  change (prod_powers_aux powers (a :: l))
    with (multipliers a ^ Z.of_nat (powers a) * prod_powers_aux powers l)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
IHl: Forall (λ i : index, (multipliers i > 0)%Z) l
→ (prod_powers_aux powers l >= 1)%Z
Hma: (multipliers a > 0)%Z
Hmpos: Forall (λ i : index, (multipliers i > 0)%Z) l
(multipliers a ^ Z.of_nat (powers a) *
 prod_powers_aux powers l >= 1)%Z
  by specialize (IHl Hmpos); lia.
Qed.

Lemma prod_powers_aux_gt (powers : index -> nat) (l : list index)
  (n : Z) (Hn : (n >= 0)%Z)
  (Hmpos : Forall (fun i => (multipliers i > n)%Z) l) :
  Exists (fun i => powers i <> 0) l -> (prod_powers_aux powers l > n)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
l: list index
n: Z
Hn: (n >= 0)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Exists (λ i : index, powers i ≠ 0) l
→ (prod_powers_aux powers l > n)%Z
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
l: list index
n: Z
Hn: (n >= 0)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Exists (λ i : index, powers i ≠ 0) l
→ (prod_powers_aux powers l > n)%Z
  revert Hmpos; induction l; [by inversion 2 |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Forall (λ i : index, (multipliers i > n)%Z) (a :: l)
→ Exists (λ i : index, powers i ≠ 0) (a :: l)
  → (prod_powers_aux powers (a :: l) > n)%Z
  change (prod_powers_aux powers (a :: l))
    with (multipliers a ^ Z.of_nat (powers a) * prod_powers_aux powers l)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Forall (λ i : index, (multipliers i > n)%Z) (a :: l)
→ Exists (λ i : index, powers i ≠ 0) (a :: l)
  → (multipliers a ^ Z.of_nat (powers a) *
     prod_powers_aux powers l > n)%Z
  rewrite Forall_cons, Exists_cons; intros [Hma Hmpos] Hppos.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Hppos: powers a ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
(multipliers a ^ Z.of_nat (powers a) *
 prod_powers_aux powers l > n)%Z
  destruct (decide (powers a = 0)).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Hppos: powers a ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
e: powers a = 0
(multipliers a ^ Z.of_nat (powers a) *
 prod_powers_aux powers l > n)%Z
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Hppos: powers a ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: powers a ≠ 0
(multipliers a ^ Z.of_nat (powers a) *
 prod_powers_aux powers l > n)%Z
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Hppos: powers a ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
e: powers a = 0
(multipliers a ^ Z.of_nat (powers a) *
 prod_powers_aux powers l > n)%Z cut (prod_powers_aux powers l > n)%Z; [by nia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Hppos: powers a ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
e: powers a = 0
(prod_powers_aux powers l > n)%Z
    apply IHl; [done |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Hppos: powers a ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
e: powers a = 0
Exists (λ i : index, powers i ≠ 0) l
    by destruct Hppos.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
Hppos: powers a ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: powers a ≠ 0
(multipliers a ^ Z.of_nat (powers a) *
 prod_powers_aux powers l > n)%Z destruct (powers a) as [| pa]; [done |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
pa: nat
Hppos: S pa ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: S pa ≠ 0
(multipliers a ^ Z.of_nat (S pa) *
 prod_powers_aux powers l > n)%Z
    replace (Z.of_nat (S pa)) with (Z.succ (Z.of_nat pa)) by lia.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
pa: nat
Hppos: S pa ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: S pa ≠ 0
(multipliers a ^ Z.succ (Z.of_nat pa) *
 prod_powers_aux powers l > n)%Z
    rewrite Z.pow_succ_r by lia.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
pa: nat
Hppos: S pa ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: S pa ≠ 0
(multipliers a * multipliers a ^ Z.of_nat pa *
 prod_powers_aux powers l > n)%Z
    cut (multipliers a ^ Z.of_nat pa * prod_powers_aux powers l >= 1)%Z; [by nia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
pa: nat
Hppos: S pa ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: S pa ≠ 0
(multipliers a ^ Z.of_nat pa *
 prod_powers_aux powers l >= 1)%Z
    cut (prod_powers_aux powers l >= 1)%Z; [by nia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
pa: nat
Hppos: S pa ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: S pa ≠ 0
(prod_powers_aux powers l >= 1)%Z
    apply prod_powers_aux_ge_1.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: Forall (λ i : index, (multipliers i > n)%Z) l
pa: nat
Hppos: S pa ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: S pa ≠ 0
Forall (λ i : index, (multipliers i > 0)%Z) l
    rewrite Forall_forall in Hmpos |- *.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
powers: index → nat
a: index
l: list index
n: Z
Hn: (n >= 0)%Z
IHl: Forall (λ i : index, (multipliers i > n)%Z) l
→ Exists (λ i : index, powers i ≠ 0) l
  → (prod_powers_aux powers l > n)%Z
Hma: (multipliers a > n)%Z
Hmpos: ∀ x : index, x ∈ l → (multipliers x > n)%Z
pa: nat
Hppos: S pa ≠ 0
∨ Exists (λ i : index, powers i ≠ 0) l
n0: S pa ≠ 0
∀ x : index, x ∈ l → (multipliers x > 0)%Z
    by intros x Hx; specialize (Hmpos x Hx); lia.
Qed.

Definition fsfun_prod (f : fsfun index 0) : Z :=
  prod_powers_aux f (fin_supp f).

#[export] Instance fsfun_prod_proper : Proper ((≡) ==> (=)) fsfun_prod.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (equiv ==> eq) fsfun_prod
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (equiv ==> eq) fsfun_prod by intros f g Heq; apply prod_powers_aux_proper, fin_supp_proper. Qed.

Lemma fsfun_prod_zero : fsfun_prod zero_fsfun = 1%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
fsfun_prod zero_fsfun = 1%Z
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
fsfun_prod zero_fsfun = 1%Z done. Qed.

Lemma fsfun_prod_succ (f : fsfun index 0) (n : index) :
  fsfun_prod (succ_fsfun f n) = (multipliers n * fsfun_prod f)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
fsfun_prod (succ_fsfun f n) =
(multipliers n * fsfun_prod f)%Z
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
fsfun_prod (succ_fsfun f n) =
(multipliers n * fsfun_prod f)%Z
  unfold fsfun_prod.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
prod_powers_aux (succ_fsfun f n)
  (fin_supp (succ_fsfun f n)) =
(multipliers n * prod_powers_aux f (fin_supp f))%Z
  destruct (decide (n ∈ fin_supp f)).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
e: n ∈ fin_supp f
prod_powers_aux (succ_fsfun f n)
  (fin_supp (succ_fsfun f n)) =
(multipliers n * prod_powers_aux f (fin_supp f))%Z
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
n0: n ∉ fin_supp f
prod_powers_aux (succ_fsfun f n)
  (fin_supp (succ_fsfun f n)) =
(multipliers n * prod_powers_aux f (fin_supp f))%Z
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
e: n ∈ fin_supp f
prod_powers_aux (succ_fsfun f n)
  (fin_supp (succ_fsfun f n)) =
(multipliers n * prod_powers_aux f (fin_supp f))%Z rewrite succ_fsfun_supp_in by done.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
e: n ∈ fin_supp f
prod_powers_aux (succ_fsfun f n) (fin_supp f) =
(multipliers n * prod_powers_aux f (fin_supp f))%Z
    revert e; specialize (fin_supp_NoDup f).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
NoDup (fin_supp f)
→ n ∈ fin_supp f
  → prod_powers_aux (succ_fsfun f n) (fin_supp f) =
    (multipliers n * prod_powers_aux f (fin_supp f))%Z
    generalize (fin_supp f) as l; clear; induction l; [by inversion 2 |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n, a: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
NoDup (a :: l)
→ n ∈ a :: l
  → prod_powers_aux (succ_fsfun f n) (a :: l) =
    (multipliers n * prod_powers_aux f (a :: l))%Z
    rewrite list.NoDup_cons, elem_of_cons; cbn.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n, a: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
(a ∉ l) ∧ NoDup l
→ n = a ∨ n ∈ l
  → (multipliers a ^ Z.of_nat (succ_fsfun f n a) *
     foldr Z.mul 1
       (zip_with Z.pow (map multipliers l)
          (map (Z.of_nat ∘ succ_fsfun f n) l)))%Z =
    (multipliers n *
     (multipliers a ^ Z.of_nat (f a) *
      foldr Z.mul 1
        (zip_with Z.pow (map multipliers l)
           (map (Z.of_nat ∘ f) l))))%Z
    intros [Ha Hnodup] [<- | Hn].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: n ∉ l
Hnodup: NoDup l
(multipliers n ^ Z.of_nat (succ_fsfun f n n) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ succ_fsfun f n) l)))%Z =
(multipliers n *
 (multipliers n ^ Z.of_nat (f n) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n, a: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: a ∉ l
Hnodup: NoDup l
Hn: n ∈ l
(multipliers a ^ Z.of_nat (succ_fsfun f n a) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ succ_fsfun f n) l)))%Z =
(multipliers n *
 (multipliers a ^ Z.of_nat (f a) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z
    +index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: n ∉ l
Hnodup: NoDup l
(multipliers n ^ Z.of_nat (succ_fsfun f n n) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ succ_fsfun f n) l)))%Z =
(multipliers n *
 (multipliers n ^ Z.of_nat (f n) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z rewrite succ_fsfun_eq, assoc by typeclasses eauto; cbn.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: n ∉ l
Hnodup: NoDup l
(multipliers n ^ Z.of_nat (S (f n)) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ succ_fsfun f n) l)))%Z =
(multipliers n * multipliers n ^ Z.of_nat (f n) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ f) l)))%Z
      f_equal; [by rewrite <- Z.pow_succ_r; lia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: n ∉ l
Hnodup: NoDup l
foldr Z.mul 1%Z
  (zip_with Z.pow (map multipliers l)
     (map (Z.of_nat ∘ succ_fsfun f n) l)) =
foldr Z.mul 1%Z
  (zip_with Z.pow (map multipliers l)
     (map (Z.of_nat ∘ f) l))
      apply prod_powers_aux_ext_forall.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: n ∉ l
Hnodup: NoDup l
∀ i : index, i ∈ l → succ_fsfun f n i = f i
      by intros; rewrite succ_fsfun_neq; [ |set_solver].
    +index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n, a: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: a ∉ l
Hnodup: NoDup l
Hn: n ∈ l
(multipliers a ^ Z.of_nat (succ_fsfun f n a) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ succ_fsfun f n) l)))%Z =
(multipliers n *
 (multipliers a ^ Z.of_nat (f a) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z rewrite succ_fsfun_neq by set_solver.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n, a: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: a ∉ l
Hnodup: NoDup l
Hn: n ∈ l
(multipliers a ^ Z.of_nat (f a) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers l)
      (map (Z.of_nat ∘ succ_fsfun f n) l)))%Z =
(multipliers n *
 (multipliers a ^ Z.of_nat (f a) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z
      setoid_rewrite IHl; [| done..].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n, a: index
l: list index
IHl: NoDup l
→ n ∈ l
  → prod_powers_aux (succ_fsfun f n) l =
    (multipliers n * prod_powers_aux f l)%Z
Ha: a ∉ l
Hnodup: NoDup l
Hn: n ∈ l
(multipliers a ^ Z.of_nat (f a) *
 (multipliers n * prod_powers_aux f l))%Z =
(multipliers n *
 (multipliers a ^ Z.of_nat (f a) *
  foldr Z.mul 1
    (zip_with Z.pow (map multipliers l)
       (map (Z.of_nat ∘ f) l))))%Z
      by unfold prod_powers_aux; lia.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
n0: n ∉ fin_supp f
prod_powers_aux (succ_fsfun f n)
  (fin_supp (succ_fsfun f n)) =
(multipliers n * prod_powers_aux f (fin_supp f))%Z rewrite succ_fsfun_supp_not_in by done.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
n0: n ∉ fin_supp f
prod_powers_aux (succ_fsfun f n) (n :: fin_supp f) =
(multipliers n * prod_powers_aux f (fin_supp f))%Z
    cbn; rewrite succ_fsfun_eq.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
n0: n ∉ fin_supp f
(multipliers n ^ Z.of_nat (S (f n)) *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers (fin_supp f))
      (map (Z.of_nat ∘ succ_fsfun f n) (fin_supp f))))%Z =
(multipliers n * prod_powers_aux f (fin_supp f))%Z
    assert (f n = 0) as -> by (rewrite elem_of_fin_supp in n0; cbn in n0; lia).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
n0: n ∉ fin_supp f
(multipliers n ^ Z.of_nat 1 *
 foldr Z.mul 1
   (zip_with Z.pow (map multipliers (fin_supp f))
      (map (Z.of_nat ∘ succ_fsfun f n) (fin_supp f))))%Z =
(multipliers n * prod_powers_aux f (fin_supp f))%Z
    cbn; f_equal; [by lia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
n0: n ∉ fin_supp f
foldr Z.mul 1%Z
  (zip_with Z.pow (map multipliers (fin_supp f))
     (map (Z.of_nat ∘ succ_fsfun f n) (fin_supp f))) =
prod_powers_aux f (fin_supp f)
    apply prod_powers_aux_ext_forall.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f: fsfun index 0
n: index
n0: n ∉ fin_supp f
∀ i : index, i ∈ fin_supp f → succ_fsfun f n i = f i
    by intros; rewrite succ_fsfun_neq; [| set_solver].
Qed.

Lemma prod_powers_delta (n : index) :
  fsfun_prod (delta_nat_fsfun n) = multipliers n.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: index
fsfun_prod (delta_nat_fsfun n) = multipliers n
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: index
fsfun_prod (delta_nat_fsfun n) = multipliers n
  intros; unfold delta_nat_fsfun.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: index
fsfun_prod (succ_fsfun zero_fsfun n) = multipliers n
  rewrite fsfun_prod_succ, fsfun_prod_zero by typeclasses eauto.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: index
(multipliers n * 1)%Z = multipliers n
  by lia.
Qed.

Lemma prod_powers_gt (n : Z) (Hn : (n >= 0)%Z)
  (Hmpos : forall (i : index), (multipliers i > n)%Z) :
  forall (f : fsfun index 0), fin_supp f <> [] ->
  (fsfun_prod f > n)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
∀ f : fsfun index 0,
  fin_supp f ≠ [] → (fsfun_prod f > n)%Z
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
∀ f : fsfun index 0,
  fin_supp f ≠ [] → (fsfun_prod f > n)%Z
  intros.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
H: fin_supp f ≠ []
(fsfun_prod f > n)%Z
  apply prod_powers_aux_gt; [done | ..].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
H: fin_supp f ≠ []
Forall (λ i : index, (multipliers i > n)%Z)
  (fin_supp f)
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
H: fin_supp f ≠ []
Exists (λ i : index, f i ≠ 0) (fin_supp f)
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
H: fin_supp f ≠ []
Forall (λ i : index, (multipliers i > n)%Z)
  (fin_supp f) by apply Forall_forall; intros; apply Hmpos.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
H: fin_supp f ≠ []
Exists (λ i : index, f i ≠ 0) (fin_supp f) apply Exists_exists.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
H: fin_supp f ≠ []
∃ x : index, x ∈ fin_supp f ∧ f x ≠ 0
    unfold fin_supp; setoid_rewrite elem_of_list_fmap.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
H: fin_supp f ≠ []
∃ x : index,
  (∃ y : {x0 : index | bool_decide (f x0 ≠ 0)},
     x = `y ∧ y ∈ enum (support 0 f)) ∧ f x ≠ 0
    destruct (fin_supp f) eqn: Heq; [done |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
i: index
l: list index
Heq: fin_supp f = i :: l
H: i :: l ≠ []
∃ x : index,
  (∃ y : {x0 : index | bool_decide (f x0 ≠ 0)},
     x = `y ∧ y ∈ enum (support 0 f)) ∧ f x ≠ 0
    assert (Hi : i ∈ fin_supp f) by (rewrite Heq; left).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
i: index
l: list index
Heq: fin_supp f = i :: l
H: i :: l ≠ []
Hi: i ∈ fin_supp f
∃ x : index,
  (∃ y : {x0 : index | bool_decide (f x0 ≠ 0)},
     x = `y ∧ y ∈ enum (support 0 f)) ∧ f x ≠ 0
    apply elem_of_list_fmap in Hi.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
i: index
l: list index
Heq: fin_supp f = i :: l
H: i :: l ≠ []
Hi: ∃ y : {x : index | bool_decide (f x ≠ 0)},
  i = `y ∧ y ∈ enum (support 0 f)
∃ x : index,
  (∃ y : {x0 : index | bool_decide (f x0 ≠ 0)},
     x = `y ∧ y ∈ enum (support 0 f)) ∧ f x ≠ 0
    eexists; split; [done |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
i: index
l: list index
Heq: fin_supp f = i :: l
H: i :: l ≠ []
Hi: ∃ y : {x : index | bool_decide (f x ≠ 0)},
  i = `y ∧ y ∈ enum (support 0 f)
f i ≠ 0
    destruct Hi as ([j Hj] & [= ->] & b).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
n: Z
Hn: (n >= 0)%Z
Hmpos: ∀ i : index, (multipliers i > n)%Z
f: fsfun index 0
l: list index
j: index
H: j :: l ≠ []
Heq: fin_supp f = j :: l
Hj: bool_decide (f j ≠ 0)
b: j ↾ Hj ∈ enum (support 0 f)
f j ≠ 0
    by eapply bool_decide_unpack.
Qed.

Lemma prod_powers_elem_of_dom :
  forall (f : fsfun index 0) (i : index),
    i ∈ fin_supp f -> (multipliers i | fsfun_prod f)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ (f : fsfun index 0) (i : index),
  i ∈ fin_supp f → (multipliers i | fsfun_prod f)%Z
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ (f : fsfun index 0) (i : index),
  i ∈ fin_supp f → (multipliers i | fsfun_prod f)%Z
  apply (nat_fsfun_ind (fun f => forall i, i ∈ fin_supp f -> (multipliers i | fsfun_prod f)%Z)).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (equiv ==> impl)
  (λ f : fsfun index 0,
     ∀ i : index,
       i ∈ fin_supp f
       → (multipliers i | fsfun_prod f)%Z)
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ i : index,
  i ∈ fin_supp zero_fsfun
  → (multipliers i | fsfun_prod zero_fsfun)%Z
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ (i : index) (f : fsfun index 0),
  (∀ i0 : index,
     i0 ∈ fin_supp f
     → (multipliers i0 | fsfun_prod f)%Z)
  → ∀ i0 : index,
      i0 ∈ fin_supp (succ_fsfun f i)
      → (multipliers i0 | fsfun_prod (succ_fsfun f i))%Z
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (equiv ==> impl)
  (λ f : fsfun index 0,
     ∀ i : index,
       i ∈ fin_supp f
       → (multipliers i | fsfun_prod f)%Z) intros f g Heq Hall i Hi.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f, g: fsfun index 0
Heq: f ≡ g
Hall: ∀ i : index,
  i ∈ fin_supp f
  → (multipliers i | fsfun_prod f)%Z
i: index
Hi: i ∈ fin_supp g
(multipliers i | fsfun_prod g)%Z
    rewrite <- Heq in Hi.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f, g: fsfun index 0
Heq: f ≡ g
Hall: ∀ i : index,
  i ∈ fin_supp f
  → (multipliers i | fsfun_prod f)%Z
i: index
Hi: i ∈ fin_supp f
(multipliers i | fsfun_prod g)%Z
    apply Hall in Hi as [x Hx].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f, g: fsfun index 0
Heq: f ≡ g
Hall: ∀ i : index,
  i ∈ fin_supp f
  → (multipliers i | fsfun_prod f)%Z
i: index
x: Z
Hx: fsfun_prod f = (x * multipliers i)%Z
(multipliers i | fsfun_prod g)%Z
    by exists x; rewrite <- Heq.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ i : index,
  i ∈ fin_supp zero_fsfun
  → (multipliers i | fsfun_prod zero_fsfun)%Z by inversion 1.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ (i : index) (f : fsfun index 0),
  (∀ i0 : index,
     i0 ∈ fin_supp f
     → (multipliers i0 | fsfun_prod f)%Z)
  → ∀ i0 : index,
      i0 ∈ fin_supp (succ_fsfun f i)
      → (multipliers i0 | fsfun_prod (succ_fsfun f i))%Z intros j f IHf i Hi.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
j: index
f: fsfun index 0
IHf: ∀ i : index,
  i ∈ fin_supp f
  → (multipliers i | fsfun_prod f)%Z
i: index
Hi: i ∈ fin_supp (succ_fsfun f j)
(multipliers i | fsfun_prod (succ_fsfun f j))%Z
    rewrite fsfun_prod_succ.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
j: index
f: fsfun index 0
IHf: ∀ i : index,
  i ∈ fin_supp f
  → (multipliers i | fsfun_prod f)%Z
i: index
Hi: i ∈ fin_supp (succ_fsfun f j)
(multipliers i | multipliers j * fsfun_prod f)%Z
    apply elem_of_succ_fsfun in Hi as [<- | Hi]; [by exists (fsfun_prod f); lia |].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
j: index
f: fsfun index 0
IHf: ∀ i : index,
  i ∈ fin_supp f
  → (multipliers i | fsfun_prod f)%Z
i: index
Hi: i ∈ fin_supp f
(multipliers i | multipliers j * fsfun_prod f)%Z
    destruct (IHf _ Hi) as [x ->].index: Type
EqDecision0: EqDecision index
multipliers: index → Z
j: index
f: fsfun index 0
IHf: ∀ i : index,
  i ∈ fin_supp f
  → (multipliers i | fsfun_prod f)%Z
i: index
Hi: i ∈ fin_supp f
x: Z
(multipliers i | multipliers j * (x * multipliers i))%Z
    by exists (multipliers j * x)%Z; lia.
Qed.

Lemma prod_powers_add :
  forall (f1 f2 : fsfun index 0),
    fsfun_prod (add_fsfun f1 f2) = (fsfun_prod f1 * fsfun_prod f2)%Z.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ f1 f2 : fsfun index 0,
  fsfun_prod (add_fsfun f1 f2) =
  (fsfun_prod f1 * fsfun_prod f2)%Z
Proof.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ f1 f2 : fsfun index 0,
  fsfun_prod (add_fsfun f1 f2) =
  (fsfun_prod f1 * fsfun_prod f2)%Z
  apply (nat_fsfun_ind (fun f1 => forall f2,
    fsfun_prod (add_fsfun f1 f2) = (fsfun_prod f1 * fsfun_prod f2)%Z)).index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (equiv ==> impl)
  (λ f1 : fsfun index 0,
     ∀ f2 : fsfun index 0,
       fsfun_prod (add_fsfun f1 f2) =
       (fsfun_prod f1 * fsfun_prod f2)%Z)
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ f2 : fsfun index 0,
  fsfun_prod (add_fsfun zero_fsfun f2) =
  (fsfun_prod zero_fsfun * fsfun_prod f2)%Z
index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ (i : index) (f : fsfun index 0),
  (∀ f2 : fsfun index 0,
     fsfun_prod (add_fsfun f f2) =
     (fsfun_prod f * fsfun_prod f2)%Z)
  → ∀ f2 : fsfun index 0,
      fsfun_prod (add_fsfun (succ_fsfun f i) f2) =
      (fsfun_prod (succ_fsfun f i) * fsfun_prod f2)%Z
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
Proper (equiv ==> impl)
  (λ f1 : fsfun index 0,
     ∀ f2 : fsfun index 0,
       fsfun_prod (add_fsfun f1 f2) =
       (fsfun_prod f1 * fsfun_prod f2)%Z) intros f f1 Heq Hall f2.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f, f1: fsfun index 0
Heq: f ≡ f1
Hall: ∀ f2 : fsfun index 0,
  fsfun_prod (add_fsfun f f2) =
  (fsfun_prod f * fsfun_prod f2)%Z
f2: fsfun index 0
fsfun_prod (add_fsfun f1 f2) =
(fsfun_prod f1 * fsfun_prod f2)%Z
    rewrite <- Heq, Hall.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f, f1: fsfun index 0
Heq: f ≡ f1
Hall: ∀ f2 : fsfun index 0,
  fsfun_prod (add_fsfun f f2) =
  (fsfun_prod f * fsfun_prod f2)%Z
f2: fsfun index 0
(fsfun_prod f * fsfun_prod f2)%Z =
(fsfun_prod f * fsfun_prod f2)%Z
    by lia.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ f2 : fsfun index 0,
  fsfun_prod (add_fsfun zero_fsfun f2) =
  (fsfun_prod zero_fsfun * fsfun_prod f2)%Z intros f2.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f2: fsfun index 0
fsfun_prod (add_fsfun zero_fsfun f2) =
(fsfun_prod zero_fsfun * fsfun_prod f2)%Z
    rewrite fsfun_prod_zero, left_id by typeclasses eauto.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
f2: fsfun index 0
fsfun_prod f2 = (1 * fsfun_prod f2)%Z
    by lia.
  -index: Type
EqDecision0: EqDecision index
multipliers: index → Z
∀ (i : index) (f : fsfun index 0),
  (∀ f2 : fsfun index 0,
     fsfun_prod (add_fsfun f f2) =
     (fsfun_prod f * fsfun_prod f2)%Z)
  → ∀ f2 : fsfun index 0,
      fsfun_prod (add_fsfun (succ_fsfun f i) f2) =
      (fsfun_prod (succ_fsfun f i) * fsfun_prod f2)%Z intros i f1 Hall f2.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
i: index
f1: fsfun index 0
Hall: ∀ f2 : fsfun index 0,
  fsfun_prod (add_fsfun f1 f2) =
  (fsfun_prod f1 * fsfun_prod f2)%Z
f2: fsfun index 0
fsfun_prod (add_fsfun (succ_fsfun f1 i) f2) =
(fsfun_prod (succ_fsfun f1 i) * fsfun_prod f2)%Z
    rewrite add_fsfun_succ_l, !fsfun_prod_succ, Hall.index: Type
EqDecision0: EqDecision index
multipliers: index → Z
i: index
f1: fsfun index 0
Hall: ∀ f2 : fsfun index 0,
  fsfun_prod (add_fsfun f1 f2) =
  (fsfun_prod f1 * fsfun_prod f2)%Z
f2: fsfun index 0
(multipliers i * (fsfun_prod f1 * fsfun_prod f2))%Z =
(multipliers i * fsfun_prod f1 * fsfun_prod f2)%Z
    by lia.
Qed.

End sec_prod_powers.

A Prime Factorization Result

#[export] Instance prime_decision : forall n, Decision (prime n) := prime_dec.

The type of prime numbers.

Definition primes : Type := dsig prime.

#[export] Program Instance primes_inhabited : Inhabited primes :=
  populate (dexist 2%Z prime_2).

Compute the product of powers of primes represented by powers. Since there are only finitely many of them, the result is well-defined.

Definition prod_primes_powers (powers : fsfun primes 0) : Z :=
  fsfun_prod (fun p : primes => ` p) powers.

Lemma not_prime_divide_prime :
  forall (n : Z),
    (n > 1)%Z -> ~ prime n ->
      exists (m : Z), prime m /\ exists (q : Z), (2 <= q < n)%Z /\ n = (q * m)%Z.∀ n : Z,
  (n > 1)%Z
  → ¬ prime n
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z)
Proof.∀ n : Z,
  (n > 1)%Z
  → ¬ prime n
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z)
  pose (P := fun n =>  ~ prime n ->
    exists (m : Z), prime m /\ exists (q : Z), (2 <= q < n)%Z /\ n = (q * m)%Z).P:= λ n : Z,
  ¬ prime n
  → ∃ m : Z,
      prime m
      ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z): Z → Prop
∀ n : Z,
  (n > 1)%Z
  → ¬ prime n
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z)
  cut (forall n : Z, (2 <= n)%Z -> P n).P:= λ n : Z,
  ¬ prime n
  → ∃ m : Z,
      prime m
      ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z): Z → Prop
(∀ n : Z, (2 ≤ n)%Z → P n)
→ ∀ n : Z,
    (n > 1)%Z
    → ¬ prime n
      → ∃ m : Z,
          prime m
          ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z)
P:= λ n : Z,
  ¬ prime n
  → ∃ m : Z,
      prime m
      ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z): Z → Prop
∀ n : Z, (2 ≤ n)%Z → P n
  {P:= λ n : Z,
  ¬ prime n
  → ∃ m : Z,
      prime m
      ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z): Z → Prop
(∀ n : Z, (2 ≤ n)%Z → P n)
→ ∀ n : Z,
    (n > 1)%Z
    → ¬ prime n
      → ∃ m : Z,
          prime m
          ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z)
    by intros HP n Hn1 Hnp; apply HP; [lia |].
  }P:= λ n : Z,
  ¬ prime n
  → ∃ m : Z,
      prime m
      ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z): Z → Prop
∀ n : Z, (2 ≤ n)%Z → P n
  apply Zlt_lower_bound_ind; subst P; cbn; intros n Hind Hn2 Hnp.n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hn2: (2 ≤ n)%Z
Hnp: ¬ prime n
∃ m : Z,
  prime m ∧ (∃ q : Z, (2 ≤ q < n)%Z ∧ n = (q * m)%Z)
  apply not_prime_divide in Hnp as (p & [Hp1 Hpn] & q & ->); [| lia].p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
∃ m : Z,
  prime m
  ∧ (∃ q0 : Z,
       (2 ≤ q0 < q * p)%Z ∧ (q * p)%Z = (q0 * m)%Z)
  destruct (decide (prime p)) as [| Hnp].p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
p0: prime p
∃ m : Z,
  prime m
  ∧ (∃ q0 : Z,
       (2 ≤ q0 < q * p)%Z ∧ (q * p)%Z = (q0 * m)%Z)
p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
Hnp: ¬ prime p
∃ m : Z,
  prime m
  ∧ (∃ q0 : Z,
       (2 ≤ q0 < q * p)%Z ∧ (q * p)%Z = (q0 * m)%Z)
  -p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
p0: prime p
∃ m : Z,
  prime m
  ∧ (∃ q0 : Z,
       (2 ≤ q0 < q * p)%Z ∧ (q * p)%Z = (q0 * m)%Z) exists p; split; [done |].p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
p0: prime p
∃ q0 : Z, (2 ≤ q0 < q * p)%Z ∧ (q * p)%Z = (q0 * p)%Z
    eexists; split; [| done].p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
p0: prime p
(2 ≤ q < q * p)%Z
    by nia.
  -p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
Hnp: ¬ prime p
∃ m : Z,
  prime m
  ∧ (∃ q0 : Z,
       (2 ≤ q0 < q * p)%Z ∧ (q * p)%Z = (q0 * m)%Z) apply Hind in Hnp as (m & Hmprime & q' & Hq' & ->); [| by lia].q, m, q': Z
Hq': (2 ≤ q' < q' * m)%Z
Hpn: (q' * m < q * (q' * m))%Z
Hp1: (1 < q' * m)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * (q' * m))%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hn2: (2 ≤ q * (q' * m))%Z
Hmprime: prime m
∃ m0 : Z,
  prime m0
  ∧ (∃ q0 : Z,
       (2 ≤ q0 < q * (q' * m))%Z
       ∧ (q * (q' * m))%Z = (q0 * m0)%Z)
    exists m; split; [done |].q, m, q': Z
Hq': (2 ≤ q' < q' * m)%Z
Hpn: (q' * m < q * (q' * m))%Z
Hp1: (1 < q' * m)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * (q' * m))%Z
  → ¬ prime y
    → ∃ m : Z,
        prime m
        ∧ (∃ q : Z,
             (2 ≤ q < y)%Z ∧ y = (q * m)%Z)
Hn2: (2 ≤ q * (q' * m))%Z
Hmprime: prime m
∃ q0 : Z,
  (2 ≤ q0 < q * (q' * m))%Z
  ∧ (q * (q' * m))%Z = (q0 * m)%Z
    by exists (q * q')%Z; split; nia.
Qed.

Lemma primes_factorization :
  forall (n : Z),
    (n > 1)%Z ->
    exists (ps : fsfun primes 0),
      fin_supp ps <> [] /\ n = prod_primes_powers ps.∀ n : Z,
  (n > 1)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ [] ∧ n = prod_primes_powers ps
Proof.∀ n : Z,
  (n > 1)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ [] ∧ n = prod_primes_powers ps
  intros n H_n.n: Z
H_n: (n > 1)%Z
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ n = prod_primes_powers ps
  assert (Hn : (2 <= n)%Z) by lia; clear H_n.n: Z
Hn: (2 ≤ n)%Z
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ n = prod_primes_powers ps
  revert n Hn; apply Zlt_lower_bound_ind; intros n Hind Hn2.n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ n)%Z
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ n = prod_primes_powers ps
  destruct (decide (prime n)) as [| Hnp].n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ n)%Z
p: prime n
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ n = prod_primes_powers ps
n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ n)%Z
Hnp: ¬ prime n
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ n = prod_primes_powers ps
  -n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ n)%Z
p: prime n
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ n = prod_primes_powers ps exists (delta_nat_fsfun (dexist n p)).n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ n)%Z
p: prime n
fin_supp (delta_nat_fsfun (dexist n p)) ≠ []
∧ n =
  prod_primes_powers (delta_nat_fsfun (dexist n p))
    split; [| by unfold prod_primes_powers; rewrite prod_powers_delta].n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ n)%Z
p: prime n
fin_supp (delta_nat_fsfun (dexist n p)) ≠ []
    by eapply elem_of_not_nil, elem_of_delta_nat_fsfun.
  -n: Z
Hind: ∀ y : Z,
  (2 ≤ y < n)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ n)%Z
Hnp: ¬ prime n
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ n = prod_primes_powers ps apply not_prime_divide in Hnp as (p & [Hp1 Hpn] & q & ->); [| lia].p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ (q * p)%Z = prod_primes_powers ps
    assert (Hq1 : (1 < q)%Z) by nia.p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
Hq1: (1 < q)%Z
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ (q * p)%Z = prod_primes_powers ps
    assert (Hqn : (q < q * p)%Z) by nia.p, q: Z
Hn2: (2 ≤ q * p)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * p)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hp1: (1 < p)%Z
Hpn: (p < q * p)%Z
Hq1: (1 < q)%Z
Hqn: (q < q * p)%Z
∃ ps : fsfun primes 0,
  fin_supp ps ≠ [] ∧ (q * p)%Z = prod_primes_powers ps
    destruct (Hind p) as (ps & Hdomps & ->); [by lia |].q: Z
ps: fsfun primes 0
Hpn: (prod_primes_powers ps <
 q * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y < q * prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hn2: (2 ≤ q * prod_primes_powers ps)%Z
Hq1: (1 < q)%Z
Hqn: (q < q * prod_primes_powers ps)%Z
Hdomps: fin_supp ps ≠ []
∃ ps0 : fsfun primes 0,
  fin_supp ps0 ≠ []
  ∧ (q * prod_primes_powers ps)%Z =
    prod_primes_powers ps0
    destruct (Hind q) as (qs & Hdomqs & ->); [by lia |].ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: fin_supp ps ≠ []
Hdomqs: fin_supp qs ≠ []
∃ ps0 : fsfun primes 0,
  fin_supp ps0 ≠ []
  ∧ (prod_primes_powers qs * prod_primes_powers ps)%Z =
    prod_primes_powers ps0
    exists (add_fsfun qs ps).ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: fin_supp ps ≠ []
Hdomqs: fin_supp qs ≠ []
fin_supp (add_fsfun qs ps) ≠ []
∧ (prod_primes_powers qs * prod_primes_powers ps)%Z =
  prod_primes_powers (add_fsfun qs ps)
    split.ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: fin_supp ps ≠ []
Hdomqs: fin_supp qs ≠ []
fin_supp (add_fsfun qs ps) ≠ []
ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: fin_supp ps ≠ []
Hdomqs: fin_supp qs ≠ []
(prod_primes_powers qs * prod_primes_powers ps)%Z =
prod_primes_powers (add_fsfun qs ps)
    +ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: fin_supp ps ≠ []
Hdomqs: fin_supp qs ≠ []
fin_supp (add_fsfun qs ps) ≠ [] apply not_null_element in Hdomps.ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: dsig (λ i : primes, i ∈ fin_supp ps)
Hdomqs: fin_supp qs ≠ []
fin_supp (add_fsfun qs ps) ≠ []
      destruct_dec_sig Hdomps i Hi Heq.ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: dsig (λ i : primes, i ∈ fin_supp ps)
Hdomqs: fin_supp qs ≠ []
i: primes
Hi: i ∈ fin_supp ps
Heq: Hdomps = dexist i Hi
fin_supp (add_fsfun qs ps) ≠ []
      by eapply elem_of_not_nil, elem_of_add_fsfun; right.
    +ps, qs: fsfun primes 0
Hpn: (prod_primes_powers ps <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hp1: (1 < prod_primes_powers ps)%Z
Hqn: (prod_primes_powers qs <
 prod_primes_powers qs * prod_primes_powers ps)%Z
Hq1: (1 < prod_primes_powers qs)%Z
Hn2: (2
 ≤ prod_primes_powers qs * prod_primes_powers ps)%Z
Hind: ∀ y : Z,
  (2 ≤ y <
   prod_primes_powers qs *
   prod_primes_powers ps)%Z
  → ∃ ps : fsfun primes 0,
      fin_supp ps ≠ []
      ∧ y = prod_primes_powers ps
Hdomps: fin_supp ps ≠ []
Hdomqs: fin_supp qs ≠ []
(prod_primes_powers qs * prod_primes_powers ps)%Z =
prod_primes_powers (add_fsfun qs ps) by symmetry; apply prod_powers_add.
Qed.