proposition: Lemma sigma_zero_elim : forall f n, (sigma f n)==0->forall k, (k<n)%nat -> f k ==0.
proof: Proof. intros; apply Ueq_class; red; intros. assert (0 < sigma f n); auto. apply sigma_not_zero with k; auto. Qed.
imports: ALEA(Utheory)