proposition: Lemma sigma_strictly_positive : forall (f : E -> Z) (x : E) (l : list E), In x l -> (forall y : E, (f y >= 0)%Z) -> (f x > 0)%Z -> (sigma E l f > 0)%Z.
proof: Proof. intros f x l. elim l. simpl in |- *; intuition. intros a l0 H H0 H1 H2. simpl in |- *. case (eq_E_dec a x). intro e. rewrite e. generalize (sigma_pos E f l0 H1). intro H3. omega. intro n. generalize (H1 a). intro H3. generalize H0. simpl in |- *. intro H4. elim H4. intro; elim n; auto. intro H5. generalize (H H5 H1 H2). intro H6. omega. Qed.
imports: List fifo table reduce