proposition: Lemma lt_sigma_sigma : forall (l : list E) (f g : E -> Z), (forall x : E, (f x <= g x)%Z) -> (exists y : E, (f y < g y)%Z /\ In y l) -> (sigma l f < sigma l g)%Z.
proof: Proof. intros; elim H0; elim l; simpl in |- *; intros. elim H1; contradiction. decompose [and or] H2. rewrite H5; generalize (le_sigma_sigma l0 f g H); omega. cut (sigma l0 f < sigma l0 g)%Z. generalize (H a); omega. apply (H1 x); auto. Qed.
imports: List bibli