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