proposition: Lemma sigma_but_pos : forall (f : E -> Z) (l : list E), (forall x_ : E, (f x_ >= 0)%Z) -> (sigma_but l f >= 0)%Z.
proof: Proof. intros; elim l; simpl in |- *. omega. intros a l0 H0. case (eq_E_dec a x0); intro. auto. generalize (H a); omega. Qed.
imports: List bibli