Library probsa.util.bigop
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export notation.
(* ---------------------------------- Main ---------------------------------- *)
Lemma bigsum_distr :
∀ (t1 t2 : nat) (f : nat → R) (c : R),
∑_{t1 ≤ i ≤ t2} c × f i = c × ∑_{t1 ≤ i ≤ t2} f i.
Lemma bigsum_add :
∀ (t1 t2 : nat) (f g : nat → R),
∑_{t1 ≤ i ≤ t2} (f i + g i) = ∑_{t1 ≤ i ≤ t2} f i + ∑_{t1 ≤ i ≤ t2} g i.
From probsa.util Require Export notation.
(* ---------------------------------- Main ---------------------------------- *)
Lemma bigsum_distr :
∀ (t1 t2 : nat) (f : nat → R) (c : R),
∑_{t1 ≤ i ≤ t2} c × f i = c × ∑_{t1 ≤ i ≤ t2} f i.
Lemma bigsum_add :
∀ (t1 t2 : nat) (f g : nat → R),
∑_{t1 ≤ i ≤ t2} (f i + g i) = ∑_{t1 ≤ i ≤ t2} f i + ∑_{t1 ≤ i ≤ t2} g i.