proposition: Lemma sigma_le : forall f n k, (k<n)%nat -> f k <= sigma f n.
proof: Proof. induction n; intros. casetype False; lia. rewrite sigma_S. assert (k < n \/ k = n)%nat. lia. case H0; intros; subst; auto. apply Ole_trans with (sigma f n); auto. Qed.
imports: ALEA(Utheory)