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