From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[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 Coq Require Import Reals Lra.
From VLSM.Lib Require Import Preamble ListExtras StdppListSet.[Loading ML file coq-itauto.plugin ... done]

Utility: Measure Related Definitions and Results

The type of positive real numbers.

Definition pos_R := {r : R | (r > 0)%R}.

Definition weight_proj1_sig (w : pos_R) : R := proj1_sig w.

We can treat a positive real number as if it were an ordinary real number.

Coercion weight_proj1_sig : pos_R >-> R.

Class Measurable (V : Type) : Type := weight : V -> pos_R.

#[global] Hint Mode Measurable ! : typeclass_instances.

Section sec_measurable_props.

Context
  `{Measurable V}
  `{FinSet V Cv}
  .

Definition sum_weights (l : Cv) : R :=
  set_fold (fun v r => (proj1_sig (weight v) + r)%R) 0%R l.

Definition sum_weights_list (vs : list V) :=
  fold_right (fun v r => (proj1_sig (weight v) + r)%R) 0%R vs.

Lemma sum_weights_list_rew (l : Cv) :
  sum_weights l = sum_weights_list (elements l).V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: Cv
sum_weights l = sum_weights_list (elements l)
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: Cv
sum_weights l = sum_weights_list (elements l) done. Qed.

Lemma sum_weights_empty :
  forall (l : Cv), l ≡ ∅ -> sum_weights l = 0%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ l : Cv, l ≡ ∅ → sum_weights l = 0%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ l : Cv, l ≡ ∅ → sum_weights l = 0%R
  intros l Hl.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: Cv
Hl: l ≡ ∅
sum_weights l = 0%R
  unfold sum_weights, set_fold; cbn.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: Cv
Hl: l ≡ ∅
foldr (λ (v : V) (r : R), (`(weight v) + r)%R) 0%R
  (elements l) = 0%R
  by apply elements_empty_iff in Hl as ->.
Qed.

Lemma sum_weights_singleton :
  forall (x : V), sum_weights {[x]} = ` (weight x).V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ x : V, sum_weights {[x]} = `(weight x)
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ x : V, sum_weights {[x]} = `(weight x)
  intros; unfold sum_weights.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
x: V
set_fold (λ (v : V) (r : R), (`(weight v) + r)%R) 0%R
  {[x]} = `(weight x)
  by rewrite set_fold_singleton; lra.
Qed.

Lemma sum_weights_positive_list (l : list V) :
  (0 <= sum_weights_list l)%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: list V
(0 <= sum_weights_list l)%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: list V
(0 <= sum_weights_list l)%R
  induction l; try apply Rle_refl.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
l: list V
IHl: (0 <= sum_weights_list l)%R
(0 <= sum_weights_list (a :: l))%R
  simpl.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
l: list V
IHl: (0 <= sum_weights_list l)%R
(0 <= `(weight a) + sum_weights_list l)%R apply Rplus_le_le_0_compat; [| done].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
l: list V
IHl: (0 <= sum_weights_list l)%R
(0 <= `(weight a))%R
  destruct (weight a); cbn.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
l: list V
IHl: (0 <= sum_weights_list l)%R
x: R
r: (x > 0)%R
(0 <= x)%R
  by apply Rlt_le.
Qed.

Lemma sum_weights_positive (l : Cv) :
  (0 <= sum_weights l)%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: Cv
(0 <= sum_weights l)%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: Cv
(0 <= sum_weights l)%R
  rewrite sum_weights_list_rew.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l: Cv
(0 <= sum_weights_list (elements l))%R
  by apply sum_weights_positive_list.
Qed.

Lemma sum_weights_in_list
  : forall (v : V) (vs : list V),
  NoDup vs ->
  v ∈ vs ->
  sum_weights_list vs
  = (proj1_sig (weight v) +
  sum_weights_list (StdppListSet.set_remove v vs))%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ (v : V) (vs : list V),
  NoDup vs
  → v ∈ vs
    → sum_weights_list vs =
      (`(weight v) +
       sum_weights_list (set_remove v vs))%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ (v : V) (vs : list V),
  NoDup vs
  → v ∈ vs
    → sum_weights_list vs =
      (`(weight v) +
       sum_weights_list (set_remove v vs))%R
  induction vs; cbn; intros Hnodup Hv **; inversion Hv as [| ? ? ? Hv']; subst; clear Hv.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: NoDup vs
→ a ∈ vs
  → sum_weights_list vs =
    (`(weight a) +
     sum_weights_list (set_remove a vs))%R
Hnodup: NoDup (a :: vs)
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0
   (if decide (a = a)
    then vs
    else a :: set_remove a vs))%R
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v, a: V
vs: list V
IHvs: NoDup vs
→ v ∈ vs
  → sum_weights_list vs =
    (`(weight v) +
     sum_weights_list (set_remove v vs))%R
Hnodup: NoDup (a :: vs)
Hv': v ∈ vs
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight v) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0
   (if decide (v = a)
    then vs
    else a :: set_remove v vs))%R
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: NoDup vs
→ a ∈ vs
  → sum_weights_list vs =
    (`(weight a) +
     sum_weights_list (set_remove a vs))%R
Hnodup: NoDup (a :: vs)
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0
   (if decide (a = a)
    then vs
    else a :: set_remove a vs))%R inversion Hnodup; subst; clear Hnodup.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: NoDup vs
→ a ∈ vs
  → sum_weights_list vs =
    (`(weight a) +
     sum_weights_list (set_remove a vs))%R
H10: a ∉ vs
H11: NoDup vs
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0
   (if decide (a = a)
    then vs
    else a :: set_remove a vs))%R
    apply Rplus_eq_compat_l.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: NoDup vs
→ a ∈ vs
  → sum_weights_list vs =
    (`(weight a) +
     sum_weights_list (set_remove a vs))%R
H10: a ∉ vs
H11: NoDup vs
foldr (λ (v : V) (r : R), (`(weight v) + r)%R) 0%R vs =
foldr (λ (v : V) (r : R), (`(weight v) + r)%R) 0%R
  (if decide (a = a) then vs else a :: set_remove a vs)
    by rewrite decide_True.
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v, a: V
vs: list V
IHvs: NoDup vs
→ v ∈ vs
  → sum_weights_list vs =
    (`(weight v) +
     sum_weights_list (set_remove v vs))%R
Hnodup: NoDup (a :: vs)
Hv': v ∈ vs
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight v) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0
   (if decide (v = a)
    then vs
    else a :: set_remove v vs))%R inversion Hnodup as [| ? ? Ha Hnodup']; subst; clear Hnodup.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v, a: V
vs: list V
IHvs: NoDup vs
→ v ∈ vs
  → sum_weights_list vs =
    (`(weight v) +
     sum_weights_list (set_remove v vs))%R
Hv': v ∈ vs
Ha: a ∉ vs
Hnodup': NoDup vs
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight v) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0
   (if decide (v = a)
    then vs
    else a :: set_remove v vs))%R
    rewrite decide_False; cbn; [| by intros ->].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v, a: V
vs: list V
IHvs: NoDup vs
→ v ∈ vs
  → sum_weights_list vs =
    (`(weight v) +
     sum_weights_list (set_remove v vs))%R
Hv': v ∈ vs
Ha: a ∉ vs
Hnodup': NoDup vs
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight v) +
 (`(weight a) +
  foldr (λ (v : V) (r : R), `(weight v) + r) 0
    (set_remove v vs)))%R
    rewrite <- Rplus_assoc, (Rplus_comm (proj1_sig (weight v))), Rplus_assoc.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v, a: V
vs: list V
IHvs: NoDup vs
→ v ∈ vs
  → sum_weights_list vs =
    (`(weight v) +
     sum_weights_list (set_remove v vs))%R
Hv': v ∈ vs
Ha: a ∉ vs
Hnodup': NoDup vs
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs)%R =
(`(weight a) +
 (`(weight v) +
  foldr (λ (v : V) (r : R), `(weight v) + r) 0
    (set_remove v vs)))%R
    by apply Rplus_eq_compat_l, IHvs.
Qed.

Lemma sum_weights_subseteq_list
  : forall (vs vs' : list V),
  NoDup vs ->
  NoDup vs' ->
  vs ⊆ vs' ->
  (sum_weights_list vs <= sum_weights_list vs')%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <= sum_weights_list vs')%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <= sum_weights_list vs')%R
  induction vs; intros vs' Hnodup_vs Hnodup_vs' Hincl;
    [by apply sum_weights_positive_list |].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs: NoDup (a :: vs)
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
(sum_weights_list (a :: vs) <= sum_weights_list vs')%R
  pose proof (Hvs' := sum_weights_in_list a vs' Hnodup_vs').V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs: NoDup (a :: vs)
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': a ∈ vs'
→ sum_weights_list vs' =
  (`(weight a) +
   sum_weights_list (set_remove a vs'))%R
(sum_weights_list (a :: vs) <= sum_weights_list vs')%R
  spec Hvs'; [by apply Hincl; left |].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs: NoDup (a :: vs)
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
(sum_weights_list (a :: vs) <= sum_weights_list vs')%R
  rewrite Hvs'; cbn.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs: NoDup (a :: vs)
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
(`(weight a) +
 foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs <=
 `(weight a) + sum_weights_list (set_remove a vs'))%R
  apply Rplus_le_compat_l.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs: NoDup (a :: vs)
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
(foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs <=
 sum_weights_list (set_remove a vs'))%R
  inversion Hnodup_vs; subst; clear Hnodup_vs.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
(foldr (λ (v : V) (r : R), `(weight v) + r) 0 vs <=
 sum_weights_list (set_remove a vs'))%R
  apply IHvs; [done | by apply set_remove_nodup |].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
vs ⊆ set_remove a vs'
  intros v Hv.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
v: V
Hv: v ∈ vs
v ∈ set_remove a vs'
  apply StdppListSet.set_remove_iff; [done |].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
v: V
Hv: v ∈ vs
v ∈ vs' ∧ v ≠ a
  split.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
v: V
Hv: v ∈ vs
v ∈ vs'
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
v: V
Hv: v ∈ vs
v ≠ a
  +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
v: V
Hv: v ∈ vs
v ∈ vs' by apply Hincl; right.
  +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
a: V
vs: list V
IHvs: ∀ vs' : list V,
  NoDup vs
  → NoDup vs'
    → vs ⊆ vs'
      → (sum_weights_list vs <=
         sum_weights_list vs')%R
vs': list V
Hnodup_vs': NoDup vs'
Hincl: a :: vs ⊆ vs'
Hvs': sum_weights_list vs' =
(`(weight a) +
 sum_weights_list (set_remove a vs'))%R
H10: a ∉ vs
H11: NoDup vs
v: V
Hv: v ∈ vs
v ≠ a by intros ->.
Qed.

Lemma sum_weights_subseteq
  : forall (vs vs' : Cv),
  vs ⊆ vs' ->
  (sum_weights vs <= sum_weights vs')%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : Cv,
  vs ⊆ vs' → (sum_weights vs <= sum_weights vs')%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : Cv,
  vs ⊆ vs' → (sum_weights vs <= sum_weights vs')%R
  intros vs vs' Hincl.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
(sum_weights vs <= sum_weights vs')%R
  rewrite !sum_weights_list_rew.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
(sum_weights_list (elements vs) <=
 sum_weights_list (elements vs'))%R
  apply sum_weights_subseteq_list.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
NoDup (elements vs)
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
NoDup (elements vs')
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
elements vs ⊆ elements vs'
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
NoDup (elements vs) by apply NoDup_elements.
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
NoDup (elements vs') by apply NoDup_elements.
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hincl: vs ⊆ vs'
elements vs ⊆ elements vs' by intro v; rewrite !elem_of_elements; apply Hincl.
Qed.

Lemma sum_weights_proper : Proper (equiv ==> eq) sum_weights.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
Proper (equiv ==> eq) sum_weights
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
Proper (equiv ==> eq) sum_weights
  intros x y Hequiv.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
x, y: Cv
Hequiv: x ≡ y
sum_weights x = sum_weights y
  by apply Rle_antisym; apply sum_weights_subseteq; intro a; apply Hequiv.
Qed.

Lemma sum_weights_in :
  forall v (vs : Cv),
    v ∈ vs -> sum_weights vs = (proj1_sig (weight v) + sum_weights (vs ∖ {[ v ]}))%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ (v : V) (vs : Cv),
  v ∈ vs
  → sum_weights vs =
    (`(weight v) + sum_weights (vs ∖ {[v]}))%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ (v : V) (vs : Cv),
  v ∈ vs
  → sum_weights vs =
    (`(weight v) + sum_weights (vs ∖ {[v]}))%R
  intros v vs Hv.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
sum_weights vs =
(`(weight v) + sum_weights (vs ∖ {[v]}))%R
  rewrite sum_weights_list_rew, sum_weights_in_list with (v := v); cycle 1.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (elements vs)
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
v ∈ elements vs
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
(`(weight v) +
 sum_weights_list (set_remove v (elements vs)))%R =
(`(weight v) + sum_weights (vs ∖ {[v]}))%R
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (elements vs) by apply NoDup_elements.
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
v ∈ elements vs by apply elem_of_elements.
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
(`(weight v) +
 sum_weights_list (set_remove v (elements vs)))%R =
(`(weight v) + sum_weights (vs ∖ {[v]}))%R apply Rplus_eq_compat_l, Rle_antisym; apply sum_weights_subseteq_list.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (set_remove v (elements vs))
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (elements (vs ∖ {[v]}))
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
set_remove v (elements vs) ⊆ elements (vs ∖ {[v]})
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (elements (vs ∖ {[v]}))
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (set_remove v (elements vs))
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
elements (vs ∖ {[v]}) ⊆ set_remove v (elements vs)
    +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (set_remove v (elements vs)) by apply set_remove_nodup, NoDup_elements.
    +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (elements (vs ∖ {[v]})) by apply NoDup_elements.
    +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
set_remove v (elements vs) ⊆ elements (vs ∖ {[v]}) intros x Hx.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
x: V
Hx: x ∈ set_remove v (elements vs)
x ∈ elements (vs ∖ {[v]})
      rewrite elem_of_elements.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
x: V
Hx: x ∈ set_remove v (elements vs)
x ∈ vs ∖ {[v]}
      apply StdppListSet.set_remove_iff in Hx; [| by apply NoDup_elements].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
x: V
Hx: x ∈ elements vs ∧ x ≠ v
x ∈ vs ∖ {[v]}
      rewrite elem_of_elements in Hx.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
x: V
Hx: x ∈ vs ∧ x ≠ v
x ∈ vs ∖ {[v]}
      by rewrite elem_of_difference, elem_of_singleton.
    +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (elements (vs ∖ {[v]})) by apply NoDup_elements.
    +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
NoDup (set_remove v (elements vs)) by apply set_remove_nodup, NoDup_elements.
    +V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
elements (vs ∖ {[v]}) ⊆ set_remove v (elements vs) intros x Hx.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
x: V
Hx: x ∈ elements (vs ∖ {[v]})
x ∈ set_remove v (elements vs)
      rewrite elem_of_elements, elem_of_difference, elem_of_singleton in Hx.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
x: V
Hx: x ∈ vs ∧ x ≠ v
x ∈ set_remove v (elements vs)
      apply StdppListSet.set_remove_iff; [by apply NoDup_elements |].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
v: V
vs: Cv
Hv: v ∈ vs
x: V
Hx: x ∈ vs ∧ x ≠ v
x ∈ elements vs ∧ x ≠ v
      by rewrite elem_of_elements.
Qed.

Lemma sum_weights_app_list
  : forall (vs vs' : list V),
  sum_weights_list (vs ++ vs') = (sum_weights_list vs + sum_weights_list vs')%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : list V,
  sum_weights_list (vs ++ vs') =
  (sum_weights_list vs + sum_weights_list vs')%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : list V,
  sum_weights_list (vs ++ vs') =
  (sum_weights_list vs + sum_weights_list vs')%R by induction vs; intros; simpl; [| rewrite IHvs]; lra. Qed.

#[export] Instance sum_weights_list_permutation_proper :
  Proper ((≡ₚ) ==> (=)) sum_weights_list.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
Proper (Permutation ==> eq) sum_weights_list
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
Proper (Permutation ==> eq) sum_weights_list
  intros l1 l2 Hl.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l1, l2: list V
Hl: l1 ≡ₚ l2
sum_weights_list l1 = sum_weights_list l2
  unfold sum_weights_list; apply foldr_permutation_proper; [.. | done].V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l1, l2: list V
Hl: l1 ≡ₚ l2
PreOrder eq
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l1, l2: list V
Hl: l1 ≡ₚ l2
∀ x : V,
  Proper (eq ==> eq) (λ r : R, (`(weight x) + r)%R)
V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l1, l2: list V
Hl: l1 ≡ₚ l2
∀ (a1 a2 : V) (b : R),
  (`(weight a1) + (`(weight a2) + b))%R =
  (`(weight a2) + (`(weight a1) + b))%R
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l1, l2: list V
Hl: l1 ≡ₚ l2
PreOrder eq by typeclasses eauto.
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l1, l2: list V
Hl: l1 ≡ₚ l2
∀ x : V,
  Proper (eq ==> eq) (λ r : R, (`(weight x) + r)%R) by congruence.
  -V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
l1, l2: list V
Hl: l1 ≡ₚ l2
∀ (a1 a2 : V) (b : R),
  (`(weight a1) + (`(weight a2) + b))%R =
  (`(weight a2) + (`(weight a1) + b))%R by intros; lra.
Qed.

Lemma sum_weights_disj_union :
  forall (vs vs' : Cv),
    vs ## vs' ->
    sum_weights (vs ∪ vs') = (sum_weights vs + sum_weights vs')%R.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : Cv,
  vs ## vs'
  → sum_weights (vs ∪ vs') =
    (sum_weights vs + sum_weights vs')%R
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
∀ vs vs' : Cv,
  vs ## vs'
  → sum_weights (vs ∪ vs') =
    (sum_weights vs + sum_weights vs')%R
  intros vs vs' Hdisj.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hdisj: vs ## vs'
sum_weights (vs ∪ vs') =
(sum_weights vs + sum_weights vs')%R
  apply elements_disj_union, sum_weights_list_permutation_proper in Hdisj.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hdisj: sum_weights_list (elements (vs ∪ vs')) =
sum_weights_list (elements vs ++ elements vs')
sum_weights (vs ∪ vs') =
(sum_weights vs + sum_weights vs')%R
  setoid_rewrite Hdisj.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs, vs': Cv
Hdisj: sum_weights_list (elements (vs ∪ vs')) =
sum_weights_list (elements vs ++ elements vs')
sum_weights_list (elements vs ++ elements vs') =
(sum_weights vs + sum_weights vs')%R
  apply sum_weights_app_list.
Qed.

Lemma sum_weights_union_empty (vs : Cv) :
  sum_weights (vs ∪ ∅) = sum_weights vs.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs: Cv
sum_weights (vs ∪ ∅) = sum_weights vs
Proof.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs: Cv
sum_weights (vs ∪ ∅) = sum_weights vs
  rewrite sum_weights_disj_union by apply disjoint_empty_r.V: Type
H: Measurable V
Cv: Type
H0: ElemOf V Cv
H1: Empty Cv
H2: Singleton V Cv
H3: Union Cv
H4: Intersection Cv
H5: Difference Cv
H6: Elements V Cv
EqDecision0: EqDecision V
H7: FinSet V Cv
vs: Cv
(sum_weights vs + sum_weights ∅)%R = sum_weights vs
  by rewrite (sum_weights_empty ∅); [lra |].
Qed.

End sec_measurable_props.