proposition: Lemma le_sigma : forall (l : list E) (f : E -> Z) (x : E), (forall x_ : E, (f x_ >= 0)%Z) -> In x l -> (f x <= sigma l f)%Z.
proof: Proof. simple induction l; simpl in |- *; intros. contradiction. decompose [or] H1. rewrite H2; generalize (sigma_pos f l0 H0); omega. generalize (H0 a); generalize (H f x H0 H2); omega. Qed.
imports: List bibli