proposition: Lemma ge_sigma_sigma : forall (l : list E) (f g : E -> Z), (forall x : E, (f x >= g x)%Z) -> (sigma l f >= sigma l g)%Z.
proof: Proof. intros; apply Zle_ge; apply le_sigma_sigma; intros; apply Zge_le; trivial. Qed.
imports: List bibli