proposition: Remark le_sigma_sigma : forall (l : list E) (f g : E -> Z), (forall x : E, (f x <= g x)%Z) -> (sigma l f <= sigma l g)%Z.
proof: Proof. simple induction l; simpl in |- *; intros. trivial with zarith. generalize (H f g H0); generalize (H0 a); omega. Qed.
imports: List bibli