proposition: Lemma sigma_minus_decr : forall f n, (forall k, f (S k) <= f k) -> sigma (fun k => f k - f (S k)) n == f O - f n.
proof: Proof. intros f n fmon;induction n. rewrite sigma_0; auto. rewrite sigma_S; rewrite IHn. rewrite Uplus_sym. rewrite Uplus_minus_assoc_right; auto. rewrite Uminus_plus_simpl; auto. elim n; intros; auto. apply Ole_trans with (f n0); auto. Qed.
imports: ALEA(Utheory)